src/HOL/Codatatype/Tools/bnf_lfp.ML

         (fld_induct2N, [fld_induct2_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
-        [(fld_iterN, iter_thms),
+        [(fld_itersN, iter_thms),
         (fld_iter_uniqueN, iter_unique_thms),
-        (fld_recN, rec_thms),
+        (fld_recsN, rec_thms),
         (unf_fldN, unf_fld_thms),
         (fld_unfN, fld_unf_thms),
         (unf_injectN, unf_inject_thms),
         (unf_exhaustN, unf_exhaust_thms),
         (fld_injectN, fld_inject_thms),