--- a/QuotMain.thy	Thu Nov 26 20:32:56 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 21:01:53 2009 +0100
@@ -221,7 +221,13 @@
 
 ML {*
 fun simp_ids lthy thm =
-  MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
+let 
+  val thms = @{thms eq_reflection[OF FUN_MAP_I] 
+                    eq_reflection[OF id_apply] 
+                    id_def_sym prod_fun_id map_id} 
+in
+  MetaSimplifier.rewrite_rule thms thm
+end
 *}
 
 section {* Does the same as 'subst' in a given theorem *}
@@ -238,7 +244,7 @@
     val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
     val rt = Goal.prove_internal [] cgoal (fn _ => tac);
   in
-    @{thm Pure.equal_elim_rule1} OF [rt, thm]
+    @{thm equal_elim_rule1} OF [rt, thm]
   end
 *}
 
@@ -312,11 +318,7 @@
 
 
 
-(******************************************)
-(******************************************)
-(* version with explicit qtrm             *)
-(******************************************)
-(******************************************)
+section {* Regularization *} 
 
 
 ML {*
@@ -737,15 +739,18 @@
 
 ML {*
 fun quotient_tac quot_thm =
+let
+  val simps = @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] 
+                     id_def_sym prod_fun_id map_id}
+in
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
     (* For functional identity quotients, (op = ---> op =) *)
-    CHANGED' (
-      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
-      )))
+    CHANGED' (simp_tac (HOL_ss addsimps simps))
   ])
+end
 *}
 
 ML {*
@@ -1211,7 +1216,9 @@
   end)  
 *}
 
-(* General outline of the lifting procedure *)
+section {* General outline of the lifting procedure *}
+
+
 (* **************************************** *)
 (*                                          *)
 (* - A is the original raw theorem          *)