Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
authorblanchet
Tue, 10 Feb 2009 14:20:47 +0100
changeset 29870 2dea33c62da7
parent 29869 a7a8b90cd882
child 29871 74366d50cf2b
Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
src/HOL/Tools/old_primrec_package.ML
--- 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