exchanged HOL_ss for HOL_basic_ss in the simplification
authorurbanc
Sun Nov 13 20:33:36 2005 +0100 (2005-11-13)
changeset 1815772e1956440ad
parent 18156 5a971b272f78
child 18158 57cba2a340f2
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
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Nov 11 10:50:43 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 13 20:33:36 2005 +0100
     1.3 @@ -56,14 +56,14 @@
     1.4        end;
     1.5  
     1.6      val simplify_rule =
     1.7 -      Simplifier.full_simplify (HOL_basic_ss addsimps
     1.8 +      Simplifier.full_simplify (HOL_ss addsimps
     1.9          [split_conv, split_paired_All, split_paired_all]);
    1.10  
    1.11    in
    1.12      rule
    1.13      |> inst_rule
    1.14      |> Method.multi_resolve facts1
    1.15 -    |> Seq.map simplify_rule
    1.16 +    |> Seq.map simplify_rule 
    1.17      |> Seq.map (RuleCases.save rule)
    1.18      |> Seq.map RuleCases.add
    1.19      |> Seq.map (fn (r, (cases, _)) =>