--- a/Quot/quotient_tacs.ML	Wed Jan 27 07:49:43 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 27 08:20:31 2010 +0100
@@ -98,12 +98,12 @@
 *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
 let
+  val thy = ProofContext.theory_of ctxt
   fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
-  val thy = ProofContext.theory_of ctxt
-  val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
-  val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
+  val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
+  val trm_inst = map (SOME o cterm_of thy) [R2, R1]
 in
-  case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of
+  case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
     NONE => NONE
   | SOME thm' =>
       (case try (get_match_inst thy (get_lhs thm')) redex of
@@ -425,7 +425,7 @@
 
 (*** Cleaning of the Theorem ***)
 
-(* expands all fun_maps, except in front of the bound variables listed in xs *)
+(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
 fun fun_map_simple_conv xs ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
@@ -443,7 +443,7 @@
 
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 
-
+(* custom matching functions *)
 fun mk_abs u i t =
   if incr_boundvars i u aconv t then Bound i
   else (case t of
@@ -484,16 +484,16 @@
         val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
-        val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
-        val ts = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} te
+        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+        val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
+        val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
         val (insp, inst) =
           if ty_c = ty_d
-          then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
-          else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
-        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+          then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
+          else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
+        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
       in
-        Conv.rewr_conv ti ctrm
+        Conv.rewr_conv thm4 ctrm
       end
   | _ => Conv.all_conv ctrm
 
@@ -504,14 +504,18 @@
 (* Cleaning consists of:
 
   1. unfolding of ---> in front of everything, except
-     bound variables
-     (this prevents lambda_prs from becoming stuck)
+     bound variables (this prevents lambda_prs from 
+     becoming stuck)
 
   2. simplification with lambda_prs
 
-  3. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
-     folding of definitions and preservation lemmas;
-     and simplification with babs_prs all_prs ex_prs ex1_prs
+  3. simplification with: 
+
+      - Quotient_abs_rep Quotient_rel_rep 
+        babs_prs all_prs ex_prs ex1_prs
+      - id_simps
+     
+     and folding of definitions and preservation lemmas
 
   4. test for refl
 *)
@@ -521,9 +525,9 @@
   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy
+  val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
 
-  fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-  val ss = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs)
+  val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
 in
   EVERY' [fun_map_tac lthy,
           lambda_prs_tac lthy,