--- a/FSet.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/FSet.thy	Sat Oct 31 11:20:55 2009 +0100
@@ -356,18 +356,10 @@
 
 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"
-  apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
-done
-
-ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
-ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *}
-ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
-ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
-ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
+ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) 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 ind_r_a = simp_allex_prs @{context} quot ind_r_l *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}