--- a/FSet.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/FSet.thy	Tue Nov 03 17:30:27 2009 +0100
@@ -301,7 +301,7 @@
 
 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" *}
+ML {* val (trans2, reps_same, absrep, 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}
@@ -358,9 +358,6 @@
 
 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_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
-thm APP_PRS
-ML aps
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}