 		[(old->new A) (set (map #(substitute % old->new) def-A))]))
      old->new]))
 
-(defn- conjunctors
-  "Returns the elements of the dl-expression connected by
-  conjunction. If the dl-expression is not a conjunction the singelton
-  set containing the expression is returned."
-  [dl-expr]
-  (if (and (compound? dl-expr)
-	   (= 'and (operator dl-expr)))
-    (set (arguments dl-expr))
-    (set [dl-expr])))
-
 (defn- tbox->hash-map
   "Transforms given TBox to a hash-map of defined concepts to the sets
   of concepts in the top-level conjunction."

		      (make-dl-definition language A (cons 'and def-A)))]
    (make-tbox language (set definitions))))

(defn- normalize-for-goal
  "If term satisfies goal, regards it as being normalized. Otherwise
  handles term as tbox and finally introduces a new symbol defining
  term."
  [term goal]
  (cond
   (goal term) [term {}]
   (tbox-target-pair? term) (let [[tbox target] (expression term),
				  [tbox-map trans] (uniquify-tbox-map (tbox->hash-map tbox))]
			      [(trans target) tbox-map])
   :else (let [new-sym (gensym)]
	   [new-sym {new-sym (conjunctors term)}])))

(defn- introduce-auxiliary-definitions
  "Introduces auxiliary definitions into the given tbox-map (as

    (.write out (.trim output))))

;;; Normalizing

(defn- conjunctors
  "Returns the elements of the dl-expression connected by
  conjunction. If the dl-expression is not a conjunction the singelton
  set containing the expression is returned."
  [dl-expr]
  (if (and (compound? dl-expr)
	   (= 'and (operator dl-expr)))
    (set (arguments dl-expr))
    (set [dl-expr])))

;; tboxes as hash-maps

(defn- uniquify-tbox-map
  "Renames all defined concepts in the given tbox-map to be globally
