src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
-            co_inducts co_rec_thms disc_corec_thms sel_corec_thmss =
+            co_inducts co_rec_thms disc_corec_thms sel_corec_thmss rel_injects =
           {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
            absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
            ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
            maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
            co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
-           sel_co_recss = sel_corec_thmss}
+           sel_co_recss = sel_corec_thmss, rel_injects = rel_injects}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
-          map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss;
+          map15 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+            co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss
+            (map #rel_injects fp_sugars0);
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
         (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
       end)