changeset 33056 | 791a4655cae3 |
parent 33040 | cffdb7b28498 |
child 33317 | b4534348b8fd |
--- a/src/HOL/Tools/old_primrec.ML Wed Oct 21 16:57:57 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Wed Oct 21 17:34:35 2009 +0200 @@ -284,7 +284,7 @@ in thy'' |> note (("simps", - [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'') + [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'') |> snd |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd