# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259959409 -3600
# Node ID 51a1d1aba9fd93b8e2b93512920e6b1dc824387e
# Parent  f178958d3d816a671030c031e89cf8cb02a03cca# Parent  9fb773ec083c0dbf16f14df0ea46112d8bacbee6
merged

diff -r f178958d3d81 -r 51a1d1aba9fd FSet.thy
diff -r f178958d3d81 -r 51a1d1aba9fd QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 21:42:55 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 21:43:29 2009 +0100
@@ -937,20 +937,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)
@@ -1240,41 +1238,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