--- a/FSet.thy	Fri Dec 04 19:06:53 2009 +0100
+++ b/FSet.thy	Fri Dec 04 19:47:58 2009 +0100
@@ -297,10 +297,6 @@
 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 19:06:53 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 19:47:58 2009 +0100
@@ -882,20 +882,18 @@
 *}
 
 ML {*
-val rep_abs_rsp_tac =
-  Subgoal.FOCUS (fn {concl, context, ...} =>
-    case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) =>
+fun rep_abs_rsp_tac ctxt =
+  SUBGOAL (fn (goal, i) =>
+    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of (rel $ _ $ (rep $ (abs $ _))) =>
     (let
-      val thy = ProofContext.theory_of context;
+      val thy = ProofContext.theory_of ctxt;
       val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
       val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
       val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
       val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
-      val te = solve_quotient_assums context thm
-      val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs];
-      val thm = Drule.instantiate' [] t_inst te
+      val te = solve_quotient_assums ctxt thm
     in
-      compose_tac (false, thm, 1) 1
+      rtac te i
     end
     handle _ => no_tac)
   | _ => no_tac)