diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/simpdata.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -380,7 +380,7 @@
        if_True, if_False, if_cancel, if_eq_cancel,
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq,
+       disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
        thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]