--- a/src/HOL/simpdata.ML Thu Feb 06 18:40:39 1997 +0100
+++ b/src/HOL/simpdata.ML Fri Feb 07 14:13:20 1997 +0100
@@ -318,7 +318,8 @@
FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]);
val HOL_ss = HOL_min_ss
- addsimps ([if_True, if_False, if_cancel,
+ addsimps ([triv_forall_equality, (* prunes params *)
+ if_True, if_False, if_cancel,
o_apply, imp_disjL, conj_assoc, disj_assoc,
de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
@ ex_simps @ all_simps @ simp_thms)