# HG changeset patch
# User blanchet
# Date 1234272047 -3600
# Node ID 2dea33c62da7d7f172b3be822cc37fee97c4ebba
# Parent  a7a8b90cd882305de7edf2dadc3a54a37b441578
Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.

diff -r a7a8b90cd882 -r 2dea33c62da7 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