# HG changeset patch
# User blanchet
# Date 1256136780 -7200
# Node ID dabf9d1bb5523e4c4532c2f9ff280d05bda4a0ec
# Parent  c39860141415ecf8102f377eba5f37788a2c0d1d
removed "nitpick_const_simp" attribute from Record's "simps";
Nitpick has its own notion of a record and doesn't need those.

diff -r c39860141415 -r dabf9d1bb552 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 21 16:53:00 2009 +0200
@@ -2362,8 +2362,7 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [((Binding.name "simps", sel_upd_simps),
-            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')