src/HOL/Nominal/nominal_induct.ML
changeset 18157 72e1956440ad
parent 18099 e956b04fea22
child 18158 57cba2a340f2
     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, _)) =>