src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

             (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
              else define_coiters [unfoldN, corecN] (the coiters_args_types))
               (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
           |>> split_list;
 
-        val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
-              sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
+        val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
+              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
               xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
               co_iterss co_iter_defss lthy
-            |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
-              ([induct], fold_thmss, rec_thmss, [], [], [], []))
+            |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
+              ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
               dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
               ns ctr_defss ctr_sugars co_iterss co_iter_defss
               (Proof_Context.export lthy no_defs_lthy) lthy
             |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
                     (disc_unfold_thmss, disc_corec_thmss, _), _,
                     (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
-              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
-               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
+               disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
         fun mk_target_fp_sugar (kk, T) =
           {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
            nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
            ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
+           co_inductss = transpose co_inductss,
            co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
            disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
            sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
           |> morph_fp_sugar phi;