diff -r 7f97c52021c9 -r 767baada01dc QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 12:07:54 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 14:11:46 2009 +0100
@@ -875,6 +875,33 @@
 *}
 
 ML {*
+val APPLY_RSP_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, ty_d];
+              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
+              val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
+              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
+              (*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)
 *}
 
@@ -1019,7 +1046,8 @@
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2),
+    NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
+      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
     NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
@@ -1049,7 +1077,7 @@
                   THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' 
+    NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN'
                 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),