--- a/QuotMain.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -701,14 +701,26 @@
   | _ => fn _ => no_tac) i st
 *}
 
+ML {*
+fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+  let
+    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+    val insts = Thm.match (pat, concl)
+in
+  if needs_lift rty (type_of f) then
+    rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+  else no_tac
+end
+handle _ => no_tac)
+*}
 
 ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
-    rtac @{thm ext},
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
@@ -719,8 +731,10 @@
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
-    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},
-    (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
     rtac reflex_thm,
     atac,
     (
@@ -737,7 +751,7 @@
     val rt = build_repabs_term lthy thm constructors rty qty;
     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
-      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
   in
     (rt, cthm, thm)