src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 17:34:35 2009 +0200
@@ -372,8 +372,7 @@
          in
            lthy''
            |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
-                map (Attrib.internal o K)
-                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+                map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd
          end)