diff -r bed81795848c -r ede7f9622a54 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 10:12:17 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 10:36:35 2009 +0100
@@ -839,6 +839,53 @@
      | _ => no_tac)
 *}
 
+(* It proves the QUOTIENT assumptions by calling quotient_tac *)
+ML {*
+fun solve_quotient_assum i ctxt thm =
+  let
+    val tac =
+      (compose_tac (false, thm, i)) THEN_ALL_NEW
+      (quotient_tac ctxt);
+    val gc = Drule.strip_imp_concl (cprop_of thm);
+  in
+    Goal.prove_internal [] gc (fn _ => tac 1)
+  end
+  handle _ => error "solve_quotient_assum"
+*}
+
+ML {*
+fun solve_quotient_assums ctxt thm =
+  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
+  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+  end
+  handle _ => error "solve_quotient_assums"
+*}
+
+ML {*
+val APPLY_RSP1_TAC' =
+  Subgoal.FOCUS (fn {concl, asms, context,...} =>
+    case ((HOLogic.dest_Trueprop (term_of concl))) of
+       ((R2 $ (f $ x) $ (g $ y))) =>
+          let
+            val (asmf, asma) = find_qt_asm (map term_of asms);
+          in
+            if (fastype_of asmf) = (fastype_of f) then no_tac else let
+              val ty_a = fastype_of x;
+              val ty_b = fastype_of asma;
+              val ty_c = range_type (type_of f);
+              val thy = ProofContext.theory_of context;
+              val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+              val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1}
+              val te = solve_quotient_assums context thm
+              val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+              val thm = Drule.instantiate' [] t_inst te
+            in
+              (* TODO try sth like: compose_tac (false, thm, 1) 1 *)
+              rtac thm 1
+            end
+          end
+     | _ => no_tac)
+*}
 
 ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
@@ -1026,9 +1073,8 @@
 fun inj_repabs_tac' ctxt rel_refl trans2 =
   (FIRST' [
     inj_repabs_tac_fast ctxt trans2,
-    NDT ctxt "A" (APPLY_RSP1_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt),
-                        quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN'
+                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
@@ -1072,20 +1118,6 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
-(* It proves the QUOTIENT assumptions by calling quotient_tac *)
-ML {*
-fun solve_quotient_assum i ctxt thm =
-  let
-    val tac =
-      (compose_tac (false, thm, i)) THEN_ALL_NEW
-      (quotient_tac ctxt);
-    val gc = Drule.strip_imp_concl (cprop_of thm);
-  in
-    Goal.prove_internal [] gc (fn _ => tac 1)
-  end
-  handle _ => error "solve_quotient_assum"
-*}
-
 ML {*
 fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of