src/HOL/Tools/primrec_package.ML

       thy'
       |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     val simps'' = maps snd simps';
   in
     thy''
-    |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add NONE]), simps'')
+    |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add_default]), simps'')
     |> snd
     |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
     |> snd
     |> Theory.parent_path
     |> pair simps''