src/HOL/Tools/BNF/bnf_def.ML

            (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
            (in_bdN, [Lazy.force (#in_bd facts)]),
            (in_monoN, [Lazy.force (#in_mono facts)]),
            (in_relN, [Lazy.force (#in_rel facts)]),
            (map_comp0N, [#map_comp0 axioms]),
-           (map_transferN, [Lazy.force (#map_transfer facts)]),
            (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
            (set_map0N, #set_map0 axioms),
            (set_bdN, #set_bd axioms)] @
           (witNs ~~ wit_thmss_of_bnf bnf)

            (map_cong0N, [#map_cong0 axioms], []),
            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
            (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
            (map_idN, [Lazy.force (#map_id facts)], []),
            (map_id0N, [#map_id0 axioms], []),
+           (map_transferN, [Lazy.force (#map_transfer facts)], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
            (rel_eqN, [Lazy.force (#rel_eq facts)], []),