--- a/Quot/Examples/FSet.thy	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 22 21:06:46 2009 +0100
@@ -39,7 +39,7 @@
 
 
 ML {*
-open Quotient_Def;
+open Quotient_Term;
 *}
 
 ML {*

--- a/Quot/QuotMain.thy	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 22 21:06:46 2009 +0100
@@ -110,6 +110,11 @@
   id_o[THEN eq_reflection]
   o_id[THEN eq_reflection] 
 
+
+(* The translation functions for the lifting process. *)
+use "quotient_term.ML" 
+
+
 (* Definition of the quotient types *)
 use "quotient_typ.ML"
 
@@ -117,11 +122,6 @@
 (* Definitions for quotient constants *)
 use "quotient_def.ML"
 
-
-(* The translation functions for the lifting process. *)
-use "quotient_term.ML" 
-
-
 (* Tactics for proving the lifted theorems *)
 
 lemma eq_imp_rel:  

--- a/Quot/quotient_def.ML	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/quotient_def.ML	Tue Dec 22 21:06:46 2009 +0100
@@ -1,9 +1,6 @@
 
 signature QUOTIENT_DEF =
-sig
-  datatype flag = absF | repF
-  val get_fun: flag -> Proof.context -> typ * typ -> term
-  
+sig 
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
@@ -14,7 +11,7 @@
 struct
 
 open Quotient_Info;
-open Quotient_Type;
+open Quotient_Term;
 
 (* wrapper for define *)
 fun define name mx attr rhs lthy =
@@ -25,72 +22,6 @@
   ((rhs, thm), lthy')
 end
 
-datatype flag = absF | repF
-
-fun negF absF = repF
-  | negF repF = absF
-
-fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-
-fun mk_compose flag (trm1, trm2) = 
-  case flag of
-    absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
-  | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
-
-fun get_fun_aux lthy s fs =
-let
-  val thy = ProofContext.theory_of lthy
-  val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
-  val info = maps_lookup thy s handle NotFound => raise exc
-in
-  list_comb (Const (#mapfun info, dummyT), fs)
-end
-
-fun get_const flag lthy _ qty =
-(* FIXME: check here that the type-constructors of _ and qty are related *)
-let
-  val thy = ProofContext.theory_of lthy
-  val qty_name = Long_Name.base_name (fst (dest_Type qty))
-in
-  case flag of
-    absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
-  | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
-end
-
-
-(* calculates the aggregate abs and rep functions for a given type; 
-   repF is for constants' arguments; absF is for constants;
-   function types need to be treated specially, since repF and absF
-   change *)
-
-fun get_fun flag lthy (rty, qty) =
-  if rty = qty then mk_identity qty else
-  case (rty, qty) of
-    (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
-     let
-       val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
-       val fs_ty2 = get_fun flag lthy (ty2, ty2')
-     in
-       get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
-     end
-  | (Type (s, _), Type (s', [])) =>
-     if s = s'
-     then mk_identity qty
-     else get_const flag lthy rty qty
-  | (Type (s, tys), Type (s', tys')) =>
-     let
-        val args = map (get_fun flag lthy) (tys ~~ tys')
-     in
-        if s = s'
-        then get_fun_aux lthy s args
-        else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args)
-     end
-  | (TFree x, TFree x') =>
-     if x = x'
-     then mk_identity qty
-     else raise (LIFT_MATCH "get_fun (frees)")
-  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
-  | _ => raise (LIFT_MATCH "get_fun (default)")
 
 (* interface and syntax setup *)
 

--- a/Quot/quotient_tacs.ML	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 21:06:46 2009 +0100
@@ -12,7 +12,6 @@
 struct
 
 open Quotient_Info;
-open Quotient_Type;
 open Quotient_Term;
 
 

--- a/Quot/quotient_term.ML	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/quotient_term.ML	Tue Dec 22 21:06:46 2009 +0100
@@ -1,15 +1,87 @@
 signature QUOTIENT_TERM =
 sig
-    val regularize_trm: Proof.context -> term -> term -> term
-    val inj_repabs_trm: Proof.context -> (term * term) -> term
+   exception LIFT_MATCH of string
+ 
+   datatype flag = absF | repF
+   val get_fun: flag -> Proof.context -> typ * typ -> term
+
+   val regularize_trm: Proof.context -> term -> term -> term
+   val inj_repabs_trm: Proof.context -> (term * term) -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
 struct
 
 open Quotient_Info;
-open Quotient_Type;
-open Quotient_Def;
+
+exception LIFT_MATCH of string
+
+(* Calculates the aggregate abs and rep functions for a given type; *) 
+(* repF is for constants' arguments; absF is for constants;         *)
+(* function types need to be treated specially, since repF and absF *)
+(* change                                                           *)
+
+datatype flag = absF | repF
+
+fun negF absF = repF
+  | negF repF = absF
+
+fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+
+fun mk_compose flag (trm1, trm2) = 
+  case flag of
+    absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
+  | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
+
+fun get_fun_aux lthy s fs =
+let
+  val thy = ProofContext.theory_of lthy
+  val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
+  val info = maps_lookup thy s handle NotFound => raise exc
+in
+  list_comb (Const (#mapfun info, dummyT), fs)
+end
+
+fun get_const flag lthy _ qty =
+(* FIXME: check here that the type-constructors of _ and qty are related *)
+let
+  val thy = ProofContext.theory_of lthy
+  val qty_name = Long_Name.base_name (fst (dest_Type qty))
+in
+  case flag of
+    absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
+  | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
+end
+
+fun get_fun flag lthy (rty, qty) =
+  if rty = qty then mk_identity qty else
+  case (rty, qty) of
+    (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+     let
+       val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
+       val fs_ty2 = get_fun flag lthy (ty2, ty2')
+     in
+       get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
+     end
+  | (Type (s, _), Type (s', [])) =>
+     if s = s'
+     then mk_identity qty
+     else get_const flag lthy rty qty
+  | (Type (s, tys), Type (s', tys')) =>
+     let
+        val args = map (get_fun flag lthy) (tys ~~ tys')
+     in
+        if s = s'
+        then get_fun_aux lthy s args
+        else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args)
+     end
+  | (TFree x, TFree x') =>
+     if x = x'
+     then mk_identity qty
+     else raise (LIFT_MATCH "get_fun (frees)")
+  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
+  | _ => raise (LIFT_MATCH "get_fun (default)")
+
 
 (*
 Regularizing an rtrm means:
@@ -218,8 +290,7 @@
 *)
 
 fun mk_repabs lthy (T, T') trm = 
-  Quotient_Def.get_fun repF lthy (T, T') 
-    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+  get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm)
 
 
 (* bound variables need to be treated properly,     *)