diff -r e9cc3a3aa5d1 -r 02b14a21761a QuotMain.thy
--- a/QuotMain.thy	Thu Oct 29 17:35:03 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 11:25:29 2009 +0100
@@ -950,7 +950,46 @@
 *}
 
 ML {*
-fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let
+fun lookup_quot_data lthy qty =
+  let
+    val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy)
+    val rty = #rtyp quotdata
+    val rel = #rel quotdata
+    val rel_eqv = #equiv_thm quotdata
+    val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
+    val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
+  in
+    (rty, rel, rel_refl, rel_eqv)
+  end
+*}
+
+ML {*
+fun lookup_quot_thms lthy qty_name =
+  let
+    val thy = ProofContext.theory_of lthy;
+    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
+    val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+  in
+    (trans2, reps_same, quot)
+  end
+*}
+
+ML {*
+fun lookup_quot_consts defs =
+  let
+    fun dest_term (a $ b) = (a, b);
+    val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
+  in
+    map (fst o dest_Const o snd o dest_term) def_terms
+  end
+*}
+
+ML {*
+fun lift_thm lthy qty qty_name rsp_thms defs t = let
+  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
+  val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
+  val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
@@ -958,12 +997,14 @@
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
   val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms 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 = repeat_eqsubst_thm lthy t_defs_sym t_a;
+  val defs_sym = add_lower_defs lthy defs;
+  val t_d = repeat_eqsubst_thm lthy defs_sym t_a;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
 in
   ObjectLogic.rulify t_r
 end
 *}
 
+
 end
+