# HG changeset patch
# User blanchet
# Date 1234274295 -3600
# Node ID 74366d50cf2b5205905c32099634145553c342d6
# Parent  2dea33c62da7d7f172b3be822cc37fee97c4ebba
Added nitpick_const_simp attribute to recdef and record packages.

diff -r 2dea33c62da7 -r 74366d50cf2b src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Feb 10 14:20:47 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Feb 10 14:58:15 2009 +0100
@@ -207,7 +207,8 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Code.add_default_eqn_attribute] else [];
+    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+      Code.add_default_eqn_attribute] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy
diff -r 2dea33c62da7 -r 74366d50cf2b src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Feb 10 14:20:47 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Feb 10 14:58:15 2009 +0100
@@ -2188,7 +2188,8 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+          [((Binding.name "simps", sel_upd_simps),
+            [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme')
       |> put_sel_upd (names @ [full_moreN]) sel_upd_simps