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