# HG changeset patch
# User blanchet
# Date 1236177187 -3600
# Node ID 35518956f0ee091e2762517c398df8af62b225fc
# Parent  05d312f09a2545b963b84751533081ce7af162f4# Parent  7aec011818e0732e97889f5ea46e9aee3afb1c51
merged

diff -r 05d312f09a25 -r 35518956f0ee src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 14:23:54 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 15:33:07 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] |>