--- a/QuotMain.thy	Fri Dec 04 10:36:35 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:06:43 2009 +0100
@@ -865,26 +865,25 @@
 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);
+      ((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
-            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
+            compose_tac (false, thm, 2) 1
           end
-     | _ => no_tac)
+        end
+    | _ => no_tac)
 *}
 
 ML {*
@@ -1119,18 +1118,23 @@
 *}
 
 ML {*
+fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+  | dest_fun_type _ = error "dest_fun_type"
+*}
+
+
+ML {*
 fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
   let
-    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
-    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+    val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
+    val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
     val thy = ProofContext.theory_of ctxt;
-    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
-    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
+    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
     val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
-    val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi]
+    val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts;
     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
@@ -1141,37 +1145,35 @@
   | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
     (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
   let
-    val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+    val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
     val thy = ProofContext.theory_of ctxt;
     val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
     val tyinst = [SOME cty_a, SOME cty_b];
     val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
     val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
-    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
+    val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
   in
     Conv.rewr_conv ti ctrm
   end
   | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
     (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
   let
-    val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+    val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
     val thy = ProofContext.theory_of ctxt;
     val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
     val tyinst = [SOME cty_a, SOME cty_b];
     val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
     val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
-    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
+    val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
   in
     Conv.rewr_conv ti ctrm
   end
   | _ => Conv.all_conv ctrm
 *}
 
-(* quot stands for the QUOTIENT theorems: *)
-(* could be potentially all of them       *)
 ML {*
 val lambda_allex_prs_conv =
-  More_Conv.top_conv lambda_allex_prs_simple_conv 
+  More_Conv.top_conv lambda_allex_prs_simple_conv
 *}
 
 ML {*