src/HOL/Tools/record.ML
changeset 31902 862ae16a799d
parent 31723 f5cafe803b55
child 32091 30e2ffbba718
     1.1 --- a/src/HOL/Tools/record.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -2192,7 +2192,7 @@
     1.4        thms_thy
     1.5        |> (snd oo PureThy.add_thmss)
     1.6            [((Binding.name "simps", sel_upd_simps),
     1.7 -            [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
     1.8 +            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
     1.9             ((Binding.name "iffs", iffs), [iff_add])]
    1.10        |> put_record name (make_record_info args parent fields extension induct_scheme')
    1.11        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps