src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

 
         val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
             co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
-            ({rel_injects, rel_distincts, ...} : fp_sugar) =
+            ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
            live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
            ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
            common_co_inducts = common_co_inducts, co_inducts = co_inducts,
            co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms,
-           co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects,
-           rel_distincts = rel_distincts, fp_ctr_sugar = {}, fp_bnf_sugar = {},
+           co_rec_selss = co_rec_sel_thmss, fp_ctr_sugar = {},
+           fp_bnf_sugar = {rel_injects = rel_injects, rel_distincts = rel_distincts},
            fp_co_induct_sugar = {}}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
           map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars