src/HOL/BNF/Tools/bnf_lfp.ML

           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
         [(ctor_dtorN, ctor_dtor_thms),
         (ctor_exhaustN, ctor_exhaust_thms),
+        (ctor_foldN, ctor_fold_thms),
         (ctor_fold_uniqueN, ctor_fold_unique_thms),
-        (ctor_foldsN, ctor_fold_thms),
         (ctor_injectN, ctor_inject_thms),
-        (ctor_recsN, ctor_rec_thms),
+        (ctor_recN, ctor_rec_thms),
         (dtor_ctorN, dtor_ctor_thms),
         (dtor_exhaustN, dtor_exhaust_thms),
         (dtor_injectN, dtor_inject_thms)]
         |> map (apsnd (map single))
         |> maps (fn (thmN, thmss) =>