--- a/QuotMain.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -748,7 +748,7 @@
 *}
 
 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);
@@ -756,19 +756,7 @@
       (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
 *}
 
@@ -873,14 +861,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;