# HG changeset patch
# User blanchet
# Date 1236177177 -3600
# Node ID 7aec011818e0732e97889f5ea46e9aee3afb1c51
# Parent  aea5d7fa7ef5c14c4caf42ba85c4682d90484755
Added "nitpick_const_simp" attribute to Nominal primrec.

diff -r aea5d7fa7ef5 -r 7aec011818e0 src/HOL/Nominal/nominal_primrec.ML
--- 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] |>