src/HOL/Codatatype/Tools/bnf_gfp.ML

         (pred_coinduct_uptoN, [pred_coinduct_upto_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
-        [(unf_coiterN, coiter_thms),
+        [(unf_coitersN, coiter_thms),
         (unf_coiter_uniqueN, coiter_unique_thms),
-        (unf_corecN, corec_thms),
+        (unf_corecsN, corec_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),