Added "nitpick_const_simp" attribute to Nominal primrec.

--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 11:05:29 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 15:32:57 2009 +0100
@@ -374,7 +374,9 @@
          in
            lthy''
            |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
-             [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
+              (map (Attrib.internal o K)
+                   [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add],
+               maps snd simps')
            |> snd
          end)
       [goals] |>