src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

             injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss;
 
         val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
 
+        (* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
+           old package)? *)
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
           |> map (fn (thmN, thms, attrs) =>
               ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));