src/HOL/Nominal/nominal_primrec.ML
changeset 33056 791a4655cae3
parent 33040 cffdb7b28498
child 33171 292970b42770
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 16:57:57 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 17:34:35 2009 +0200
     1.3 @@ -372,8 +372,7 @@
     1.4           in
     1.5             lthy''
     1.6             |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
     1.7 -                map (Attrib.internal o K)
     1.8 -                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
     1.9 +                map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    1.10                  maps snd simps')
    1.11             |> snd
    1.12           end)