src/HOL/Tools/old_primrec_package.ML
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