src/HOL/Tools/BNF/bnf_def.ML

            (bd_CinfiniteN, [#bd_Cinfinite facts]),
            (bd_CnotzeroN, [#bd_Cnotzero facts]),
            (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]),
            (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 (fn (thmN, thms) =>
             ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),

       end;
 
     fun note_unless_dont_note (noted0, lthy0) =
       let
         val notes =
-          [(inj_mapN, [Lazy.force (#inj_map facts)], []),
+          [(in_relN, [Lazy.force (#in_rel facts)], []),
+           (inj_mapN, [Lazy.force (#inj_map facts)], []),
            (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
            (map_compN, [Lazy.force (#map_comp facts)], []),
            (map_cong0N, [#map_cong0 axioms], []),
            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
            (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),

            (rel_eqN, [Lazy.force (#rel_eq facts)], []),
            (rel_flipN, [Lazy.force (#rel_flip facts)], []),
            (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
            (rel_mapN, Lazy.force (#rel_map facts), []),
            (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
+           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
            (rel_transferN, [Lazy.force (#rel_transfer facts)], []),
            (set_mapN, map Lazy.force (#set_map facts), []),
            (set_transferN, Lazy.force (#set_transfer facts), [])]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>