--- 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