--- a/QuotMain.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -708,14 +708,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,
@@ -726,8 +738,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,
     (
@@ -739,27 +753,15 @@
 *}
 
 ML {*
-fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
     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)
-  end
-*}
-
-ML {*
-fun repabs_eq2 lthy (rt, thm, othm) =
-  let
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm);
-    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
-  in
-    cthm
+    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
   end
 *}
 
@@ -777,18 +779,27 @@
     val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
     val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
   in
-    Simplifier.rewrite_rule [rt] thm
+    @{thm Pure.equal_elim_rule1} OF [rt,thm]
   end
 *}
 
+ML {*
+  fun repeat_eqsubst_thm ctxt thms thm =
+    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+    handle _ => thm
+*}
+
 text {* expects atomized definition *}
 ML {*
   fun add_lower_defs_aux ctxt thm =
     let
-      val e1 = @{thm fun_cong} OF [thm]
-      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1
+      val e1 = @{thm fun_cong} OF [thm];
+      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
+      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
+      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g;
+      val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h
     in
-      thm :: (add_lower_defs_aux ctxt f)
+      thm :: (add_lower_defs_aux ctxt i)
     end
     handle _ => [thm]
 *}
@@ -855,14 +866,13 @@
 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv lthy;
-  val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-  val t_t2 = repabs_eq2 lthy t_t1;
+  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
   fun simp_lam_prs lthy thm =
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
-  val t_l = simp_lam_prs lthy t_t2;
+  val t_l = simp_lam_prs lthy t_t;
   val t_a = simp_allex_prs lthy quot t_l;
   val t_defs_sym = add_lower_defs lthy t_defs;
   val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;