changeset 28703 | aef727ef30e5 |
parent 28308 | d4396a28fb29 |
child 29266 | 4a478f9d2847 |
--- a/src/HOL/Tools/old_primrec_package.ML Tue Oct 28 12:29:57 2008 +0100 +++ b/src/HOL/Tools/old_primrec_package.ML Tue Oct 28 16:58:59 2008 +0100 @@ -284,7 +284,7 @@ val simps'' = maps snd simps'; in thy'' - |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add_default]), simps'') + |> note (("simps", [Simplifier.simp_add, Code.add_default_eqn_attribute]), simps'') |> snd |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd