--- a/QuotMain.thy	Fri Nov 27 03:33:30 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 03:56:18 2009 +0100
@@ -1047,7 +1047,7 @@
 fun inst_spec_tac ctrms =
   EVERY' (map (dtac o inst_spec) ctrms)
 
-fun abs_list xs trm = 
+fun all_list xs trm = 
   fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
 
 fun apply_under_Trueprop f = 
@@ -1059,7 +1059,7 @@
     val thy = ProofContext.theory_of ctxt
     val vrs = Term.add_frees concl []
     val cvrs = map (cterm_of thy o Free) vrs
-    val concl' = apply_under_Trueprop (abs_list vrs) concl
+    val concl' = apply_under_Trueprop (all_list vrs) concl
     val goal = Logic.mk_implies (concl', concl)
     val rule = Goal.prove ctxt [] [] goal 
       (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
@@ -1092,7 +1092,7 @@
   by simp
 
 ML {*
-fun lift_error ctxt fun_str rtrm qtrm =
+fun lift_match_error ctxt fun_str rtrm qtrm =
 let
   val rtrm_str = Syntax.string_of_term ctxt rtrm
   val qtrm_str = Syntax.string_of_term ctxt qtrm
@@ -1111,16 +1111,15 @@
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = 
         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
-        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
   val inj_goal = 
         Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
-        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
      SOME (cterm_of thy reg_goal),
-     SOME (cterm_of thy inj_goal)]
-  @{thm procedure}
+     SOME (cterm_of thy inj_goal)] @{thm procedure}
 end
 *}
 
@@ -1134,8 +1133,8 @@
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
     in
-      rtac rule THEN' rtac rthm'
-    end 1) lthy
+      EVERY1 [rtac rule, rtac rthm']
+    end) lthy
 *}
 
 ML {*
@@ -1148,12 +1147,12 @@
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val aps = find_aps (prop_of rthm') (term_of concl)
     in
-      rtac rule THEN' 
-       RANGE [rtac rthm',
-              regularize_tac lthy [rel_eqv] rel_refl,
-              REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-              clean_tac lthy quot defs reps_same absrep aps]
-    end 1) lthy
+      EVERY1 [rtac rule, 
+              RANGE [rtac rthm',
+                     regularize_tac lthy [rel_eqv] rel_refl,
+                     REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+                     clean_tac lthy quot defs reps_same absrep aps]] 
+    end) lthy
 *}
 
 end