src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

             co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
             ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
               fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
                 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
               fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
-                rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
+                co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
                 set_inducts, ...},
               ...} : 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, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
            fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,

               co_rec_discs = co_rec_disc_thms,
               co_rec_disc_iffs = co_rec_disc_iffs,
               co_rec_selss = co_rec_sel_thmss,
               co_rec_codes = co_rec_codes,
               co_rec_transfers = co_rec_transfers,
-              rec_o_maps = rec_o_maps,
+              co_rec_o_maps = co_rec_o_maps,
               common_rel_co_inducts = common_rel_co_inducts,
               rel_co_inducts = rel_co_inducts,
               common_set_inducts = common_set_inducts,
               set_inducts = set_inducts}}
           |> morph_fp_sugar phi;