# HG changeset patch
# User urbanc
# Date 1131910416 -3600
# Node ID 72e1956440ad940a64ae17244a255a54c0f8e589
# Parent  5a971b272f7823742cfffba87b2d7dd1d0c49694
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

diff -r 5a971b272f78 -r 72e1956440ad src/HOL/Nominal/nominal_induct.ML
--- 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, _)) =>