--- a/FSet.thy	Fri Dec 04 18:32:19 2009 +0100
+++ b/FSet.thy	Fri Dec 04 19:06:53 2009 +0100
@@ -297,6 +297,10 @@
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma "IN x EMPTY = False"
+
+apply(tactic {* (ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac @{context}) 1 *})
+
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

--- a/QuotMain.thy	Fri Dec 04 18:32:19 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 19:06:53 2009 +0100
@@ -1185,41 +1185,40 @@
 
 (* Left for debugging *)
 ML {*
-fun procedure_tac lthy rthm =
+fun procedure_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
-  THEN' gen_frees_tac lthy
-  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+  THEN' gen_frees_tac ctxt
+  THEN' CSUBGOAL (fn (gl, i) =>
     let
       val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
+      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
     in
-      EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1
-    end) lthy
+      (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
+    end)
 *}
 
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 
-fun lift_tac lthy rthm rel_eqv =
+fun lift_tac ctxt rthm rel_eqv =
   ObjectLogic.full_atomize_tac
-  THEN' gen_frees_tac lthy
-  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+  THEN' gen_frees_tac ctxt
+  THEN' CSUBGOAL (fn (gl, i) =>
     let
       val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
       val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv
-      val quotients = quotient_rules_get lthy
+      val quotients = quotient_rules_get ctxt
       val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
     in
-      EVERY1
-       [rtac rule,
-        RANGE [rtac rthm',
-               regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
-               clean_tac lthy]]
-    end) lthy
+      (rtac rule THEN'
+       RANGE [rtac rthm',
+              regularize_tac ctxt rel_eqv,
+              rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
+              clean_tac ctxt]) i
+    end)
 *}
 
 end