changed the HOL_basic_ss back and selectively added
simp_thms and triv_forall_equality. (Otherwise the
goals would have been simplified too much)

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