src/HOL/Tools/primrec_package.ML

     val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
     val _ = writeln ("Proving equations for primrec function(s)\n" ^
       commas names1 ^ " ...");
     val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
         (fn _ => [rtac refl 1])) eqns;
-    val tsimps = map Attribute.tthm_of char_thms;
+    val tsimps = Attribute.tthms_of char_thms;
     val thy'' = thy' |>
       PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
       PureThy.add_tthms (map (rpair [])
          (filter_out (equal "" o fst) (map fst eqns ~~ tsimps))) |>
       Theory.parent_path;