--- a/Quot/QuotMain.thy	Sat Dec 12 18:43:42 2009 +0100
+++ b/Quot/QuotMain.thy	Sun Dec 13 01:56:19 2009 +0100
@@ -669,26 +669,21 @@
     case (HOLogic.dest_Trueprop (term_of concl)) of
       (R2 $ (f $ x) $ (g $ y)) =>
         (let
-           val (asmf, asma) = find_qt_asm (map term_of asms);
+           val (asmf, asma) = find_qt_asm (map term_of asms)
          in
-           if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *)
+           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) (* why type_of, not fast_type? *)
+               val ty_c = range_type (fastype_of f) 
                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 ???   *)
+               val thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
              in
-               compose_tac (false, thm, 2) 1
+               (rtac thm THEN' quotient_tac context) 1
              end
          end
         handle ERROR "find_qt_asm: no pair" => no_tac)