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