Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
--- 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