--- a/IntEx.thy	Thu Oct 29 17:35:03 2009 +0100
+++ b/IntEx.thy	Fri Oct 30 11:25:29 2009 +0100
@@ -12,6 +12,8 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+print_theorems
+
 quotient_def (for my_int)
   ZERO::"my_int"
 where
@@ -114,21 +116,18 @@
   "(intrel ===> intrel ===> intrel) my_plus my_plus"
   by (simp)
 
-ML {* val consts = [@{const_name "my_plus"}] *}
-ML {* val rty = @{typ "nat \<times> nat"} *}
 ML {* val qty = @{typ "my_int"} *}
-ML {* val rel = @{term "intrel"} *}
-ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
-ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *}
-ML {* val quot = @{thm QUOTIENT_my_int} *}
+ML {* val ty_name = "my_int" *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
-ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *}
-ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *}
 ML {* val t_defs = @{thms PLUS_def} *}
 
 ML {*
 fun lift_thm_my_int lthy t =
-  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t
+  lift_thm lthy qty ty_name rsp_thms t_defs t
+*}
+
+ML {*
+  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty;
 *}
 
 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}