diff -r 9a3d2a4f8956 -r 44461d5615eb Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Feb 05 15:17:21 2010 +0100
+++ b/Quot/quotient_term.ML	Sat Feb 06 10:04:56 2010 +0100
@@ -473,18 +473,14 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ex1"}, ty) $ 
-      (Abs (n, _,
-        (Const (@{const_name "op &"}, _) $ 
-          (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ 
-          (t $ _)
-        )
-      )), Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
+      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ 
+        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), 
+     Const (@{const_name "Ex1"}, ty') $ t') =>
        let
-         val t = incr_boundvars (~1) t
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val t_ = incr_boundvars (~1) t
+         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-         val _ = tracing "bla"
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
@@ -689,19 +685,27 @@
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
-(*** Translating the goal automatically
+
+
+(*** Wrapper for transforming an rthm into a qthm ***)
 
+(*
 Finds subterms of a term that can be lifted and:
+
 * replaces subterms matching lifted constants by the lifted constants
+
 * replaces equivalence relations by equalities
+
 * In constants, frees and schematic variables replaces
-  subtypes matching lifted types by those types *)
+  subtypes matching lifted types by those types 
+*)
 
 fun subst_ty thy ty (rty, qty) r =
   if r <> NONE then r else
   case try (Sign.typ_match thy (ty, rty)) Vartab.empty of
     SOME inst => SOME (Envir.subst_type inst qty)
   | NONE => NONE
+
 fun subst_tys thy substs ty =
   case fold (subst_ty thy ty) substs NONE of
     SOME ty => ty
@@ -715,6 +719,7 @@
     case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
       SOME inst => SOME (Envir.subst_term inst qt)
     | NONE => NONE;
+
 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
 
 fun get_ty_trm_substs ctxt =
@@ -727,7 +732,7 @@
   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
 in
-  (ty_substs, (const_substs @ rel_substs))
+  (ty_substs, const_substs @ rel_substs)
 end
 
 fun quotient_lift_all ctxt t =
@@ -745,7 +750,7 @@
             val (y, s') = Term.dest_abs (a, ty, s)
             val nty = subst_tys thy ty_substs ty
           in
-          Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s')))
+            Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
           end
       | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
       | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)