--- a/Quot/quotient_def.ML	Tue Dec 22 21:06:46 2009 +0100
+++ b/Quot/quotient_def.ML	Tue Dec 22 21:16:11 2009 +0100
@@ -2,7 +2,7 @@
 signature QUOTIENT_DEF =
 sig 
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
-    Proof.context -> (term * thm) * local_theory
+    local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;

--- a/Quot/quotient_tacs.ML	Tue Dec 22 21:06:46 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 21:16:11 2009 +0100
@@ -14,7 +14,6 @@
 open Quotient_Info;
 open Quotient_Term;
 
-
 (* Since HOL_basic_ss is too "big" for us, we *)
 (* need to set up our own minimal simpset.    *)
 fun  mk_minimal_ss ctxt =
@@ -588,7 +587,7 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = 
-        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
+        Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm'))
         handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
   val inj_goal = 
         Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))

--- a/Quot/quotient_term.ML	Tue Dec 22 21:06:46 2009 +0100
+++ b/Quot/quotient_term.ML	Tue Dec 22 21:16:11 2009 +0100
@@ -3,9 +3,9 @@
    exception LIFT_MATCH of string
  
    datatype flag = absF | repF
-   val get_fun: flag -> Proof.context -> typ * typ -> term
+   val get_fun: flag -> Proof.context -> (typ * typ) -> term
 
-   val regularize_trm: Proof.context -> term -> term -> term
+   val regularize_trm: Proof.context -> (term * term) -> term
    val inj_repabs_trm: Proof.context -> (term * term) -> term
 end;
 
@@ -156,10 +156,10 @@
 (*   otherwise to the given term,                  *)
 (* - used by regularize, therefore abstracted      *)
 (*   variables do not have to be treated specially *)
-fun apply_subt f trm1 trm2 =
+fun apply_subt f (trm1, trm2) =
   case (trm1, trm2) of
-    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t')
-  | _ => f trm1 trm2
+    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
+  | _ => f (trm1, trm2)
 
 (* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)  
@@ -172,11 +172,11 @@
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
 
-fun regularize_trm lthy rtrm qtrm =
+fun regularize_trm lthy (rtrm, qtrm) =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (_, ty', t')) =>
        let
-         val subtrm = Abs(x, ty, regularize_trm lthy t t')
+         val subtrm = Abs(x, ty, regularize_trm lthy (t, t'))
        in
          if ty = ty' then subtrm
          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
@@ -184,7 +184,7 @@
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (regularize_trm lthy) t t'
+         val subtrm = apply_subt (regularize_trm lthy) (t, t')
        in
          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
@@ -192,7 +192,7 @@
 
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (regularize_trm lthy) t t'
+         val subtrm = apply_subt (regularize_trm lthy) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
@@ -245,7 +245,7 @@
        end 
 
   | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+       (regularize_trm lthy (t1, t1')) $ (regularize_trm lthy (t2, t2'))
 
   | (Bound i, Bound i') =>
        if i = i' then rtrm