src/HOL/Tools/primrec_package.ML

     val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
     val qualify = Binding.qualify prefix;
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add];
+      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))