# HG changeset patch
# User nipkow
# Date 855321200 -3600
# Node ID 548f8ed89a807925620341ef1360e6f92cc73c56
# Parent  4743d85eace061090fd47a9eed9c7e60802e2eea
Added "triv_forall_equality" to HOL_ss.

diff -r 4743d85eace0 -r 548f8ed89a80 src/HOL/simpdata.ML
--- 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)