src/HOL/Tools/old_primrec_package.ML
changeset 29870 2dea33c62da7
parent 29579 cb520b766e00
child 30190 479806475f3c
--- a/src/HOL/Tools/old_primrec_package.ML	Tue Feb 10 14:02:45 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Tue Feb 10 14:20:47 2009 +0100
@@ -283,7 +283,8 @@
     val simps'' = maps snd simps';
   in
     thy''
-    |> note (("simps", [Simplifier.simp_add, Code.add_default_eqn_attribute]), simps'')
+    |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+                        Code.add_default_eqn_attribute]), simps'')
     |> snd
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd