exchanged HOL_ss for HOL_basic_ss in the simplification
part. Otherwise the case where the context is instantiated
with unit leads to vacuous quantifiers, such as

ALL a. A

--- a/src/HOL/Nominal/nominal_induct.ML	Fri Nov 11 10:50:43 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 13 20:33:36 2005 +0100
@@ -56,14 +56,14 @@
       end;
 
     val simplify_rule =
-      Simplifier.full_simplify (HOL_basic_ss addsimps
+      Simplifier.full_simplify (HOL_ss addsimps
         [split_conv, split_paired_All, split_paired_all]);
 
   in
     rule
     |> inst_rule
     |> Method.multi_resolve facts1
-    |> Seq.map simplify_rule
+    |> Seq.map simplify_rule 
     |> Seq.map (RuleCases.save rule)
     |> Seq.map RuleCases.add
     |> Seq.map (fn (r, (cases, _)) =>