--- a/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:34:14 2009 +0200
@@ -283,8 +283,8 @@
val simps'' = maps snd simps';
in
thy''
- |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
- Code.add_default_eqn_attribute]), simps'')
+ |> note (("simps",
+ [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'')
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd