Added "triv_forall_equality" to HOL_ss.

--- 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)