removed "nitpick_const_simp" attribute from Record's "simps";
authorblanchet
Wed Oct 21 16:53:00 2009 +0200 (2009-10-21)
changeset 33053dabf9d1bb552
parent 32956 c39860141415
child 33054 dd1192a96968
removed "nitpick_const_simp" attribute from Record's "simps";
Nitpick has its own notion of a record and doesn't need those.
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Oct 21 16:53:00 2009 +0200
     1.3 @@ -2362,8 +2362,7 @@
     1.4      val final_thy =
     1.5        thms_thy
     1.6        |> (snd oo PureThy.add_thmss)
     1.7 -          [((Binding.name "simps", sel_upd_simps),
     1.8 -            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
     1.9 +          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
    1.10             ((Binding.name "iffs", iffs), [iff_add])]
    1.11        |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
    1.12        |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')