src/HOL/Tools/old_primrec.ML

       |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     val simps'' = maps snd simps';
   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
     |> Sign.parent_path
     |> pair simps''