--- 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)