--- a/QuotMain.thy	Tue Oct 27 07:46:52 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 09:01:12 2009 +0100
@@ -851,4 +851,25 @@
     handle _ => thm
 *}
 
+ML {*
+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 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_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;
+  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+in
+  ObjectLogic.rulify t_r
 end
+*}
+
+end