src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

         val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last
       in
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
       end;
 
-    fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) =
+    fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
       let
         val bnf = the (bnf_of lthy s);
         val live = live_of_bnf bnf;
         val mapx = mk_map live Ts Us (map_of_bnf bnf);
         val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));

               |> singleton (Proof_Context.export names_lthy lthy)
           in
             `(conj_dests nn) induct_thm
           end;
 
+        val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
+
         val (iter_thmss, rec_thmss) =
           let
             val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
             val giters = map (lists_bmoc gss) iters;
             val hrecs = map (lists_bmoc hss) recs;

                goal_iterss iter_tacss,
              map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_recss rec_tacss)
           end;
 
+        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));
+
         val common_notes =
-          (if nn > 1 then [(inductN, [induct_thm], [])] (* FIXME: attribs *) else [])
+          (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, [])]));
 
         val notes =
-          [(inductN, map single induct_thms, []), (* FIXME: attribs *)
-           (itersN, iter_thmss, simp_attrs),
-           (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
+          [(inductN, map single induct_thms,
+            fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
+           (itersN, iter_thmss, K simp_attrs),
+           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs))]
           |> maps (fn (thmN, thmss, attrs) =>
-            map2 (fn b => fn thms =>
-              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
-                [(thms, [])])) fp_bs thmss);
+            map3 (fn b => fn Type (T_name, _) => fn thms =>
+              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
+                [(thms, [])])) fp_bs fpTs thmss);
       in
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
 
     fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,