# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260639822 -3600
# Node ID 089cf9ffb711cc19d7ee1fe6a02088ca10ad6aef
# Parent  7142389632fd02f5e2b2c8d308f0b0e2ee184adb
tried to simplify apply_rsp_tac; failed at the moment; added some questions

diff -r 7142389632fd -r 089cf9ffb711 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 18:01:22 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 18:43:42 2009 +0100
@@ -666,7 +666,7 @@
 ML {*
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
-    case ((HOLogic.dest_Trueprop (term_of concl))) of
+    case (HOLogic.dest_Trueprop (term_of concl)) of
       (R2 $ (f $ x) $ (g $ y)) =>
         (let
            val (asmf, asma) = find_qt_asm (map term_of asms);
@@ -675,16 +675,18 @@
            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); (* why type_of, not fast_type? *)
-               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_rsp}
-               val te = solve_quotient_assums context thm
-               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; 
-                                                      (* why not instantiate terms 3 lines earlier *)
+               val ty_a = fastype_of x
+               val ty_b = fastype_of asma
+               val ty_c = range_type (type_of f) (* why type_of, not fast_type? *)
+               val thy = ProofContext.theory_of context
+               val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]
+               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+               val thm' = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+               val te = solve_quotient_assums context thm'
                val thm = Drule.instantiate' [] t_inst te
+                    (* why not instantiate terms 3 lines earlier *)
+                    (* \<dots> if done one gets an instantiate type conlict error ??? *)
+                    (* why is necessary to get rid of the quot-assms first ???   *)
              in
                compose_tac (false, thm, 2) 1
              end