--- a/FSet.thy	Fri Oct 30 12:22:03 2009 +0100
+++ b/FSet.thy	Fri Oct 30 14:25:37 2009 +0100
@@ -295,6 +295,7 @@
   ((map f a) ::'a list) @ (map f b)"
  by simp (rule list_eq_refl)
 
+
 ML {* val qty = @{typ "'a 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" *}
@@ -342,7 +343,10 @@
   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})) *}
+ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
+
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"