# HG changeset patch
# User urbanc
# Date 1131917790 -3600
# Node ID 57cba2a340f2c6b46168ac8caf77351fa348dedf
# Parent  72e1956440ad940a64ae17244a255a54c0f8e589
changed the HOL_basic_ss back and selectively added
simp_thms and triv_forall_equality. (Otherwise the
goals would have been simplified too much)

diff -r 72e1956440ad -r 57cba2a340f2 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sun Nov 13 20:33:36 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 13 22:36:30 2005 +0100
@@ -56,8 +56,8 @@
       end;
 
     val simplify_rule =
-      Simplifier.full_simplify (HOL_ss addsimps
-        [split_conv, split_paired_All, split_paired_all]);
+      Simplifier.full_simplify (HOL_basic_ss addsimps
+        simp_thms @ [triv_forall_equality, split_conv, split_paired_All, split_paired_all]);
 
   in
     rule