src/HOL/Tools/primrec_package.ML

--- a/src/HOL/Tools/primrec_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -251,7 +251,8 @@
       (space_implode "_" (map (Sign.base_name o #1) defs));
     val spec' = (map o apfst o apfst) qualify spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, Code.add_default_eqn_attribute];
+      [Simplifier.simp_add, Code.add_default_eqn_attribute,
+       Nitpick_Const_Simps_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())