--- a/QuotMain.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -813,6 +813,32 @@
      | _ => no_tac)
 *}
 
+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 ty_d = range_type (type_of asmf);*)
+              val thy = ProofContext.theory_of context;
+              val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c];
+              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
+              val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y];
+              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1}
+              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
+            in
+              rtac thm 1
+            end
+          end
+     | _ => no_tac)
+*}
+
 
 ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
@@ -1000,8 +1026,8 @@
 fun inj_repabs_tac' ctxt rel_refl trans2 =
   (FIRST' [
     inj_repabs_tac_fast ctxt trans2,
-    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
+    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 "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)])),