--- a/FSet.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/FSet.thy	Mon Nov 02 15:38:03 2009 +0100
@@ -367,11 +367,10 @@
 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 thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}
+ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}
-ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *}
+ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 ML {* ObjectLogic.rulify ind_r_s *}