--- a/FSet.thy	Thu Oct 29 17:35:03 2009 +0100
+++ b/FSet.thy	Fri Oct 30 11:25:29 2009 +0100
@@ -177,17 +177,9 @@
 term fmap
 thm fmap_def
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *}
-(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
-
-ML {*
-  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
-                @{const_name "membship"}, @{const_name "card1"},
-                @{const_name "append"}, @{const_name "fold1"},
-                @{const_name "map"}];
-*}
-
-ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
+ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *}
+ML {* val consts = lookup_quot_consts defs *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
 
 lemma memb_rsp:
   fixes z
@@ -303,29 +295,15 @@
   ((map f a) ::'a list) @ (map f b)"
  by simp (rule list_eq_refl)
 
-ML {* val rty = @{typ "'a list"} *}
 ML {* val qty = @{typ "'a fset"} *}
-ML {* val rel = @{term "list_eq"} *}
-ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
-ML {* val rel_refl = @{thm list_eq_refl} *}
-ML {* val quot = @{thm QUOTIENT_fset} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}
+
 ML {* val rsp_thms =
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
   @ @{thms ho_all_prs ho_ex_prs} *}
-ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
-ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
-ML {* val defs = fset_defs *}
-(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
-ML {*
-  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
-                @{const_name "membship"}, @{const_name "card1"},
-                @{const_name "append"}, @{const_name "fold1"},
-                @{const_name "map"}];
-*}
 
-ML {* fun lift_thm_fset lthy t =
-  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
-*}
+ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 by (simp add: list_eq_refl)
@@ -342,17 +320,17 @@
 thm list.recs(2)
 
 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+(*  prove {* build_regularize_goal ind_r_a rty rel @{context} *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
-        [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]),
-         (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
          (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
          (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
   apply (tactic {* tac @{context} 1 *}) *)
-ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
+ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
 ML {*
-  val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
 (*prove rg
@@ -361,9 +339,7 @@
 done*)
 ML {* val ind_r_t =
   Toplevel.program (fn () =>
-  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
-   @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
+  repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms
   )
 *}
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}

--- 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} *}

--- 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
+