src/HOL/Tools/BNF/bnf_def.ML

 open BNF_Util
 open BNF_Tactics
 open BNF_Def_Tactics
 
 val fundefcong_attrs = @{attributes [fundef_cong]};
+val mono_attrs = @{attributes [mono]};
 
 type axioms = {
   map_id0: thm,
   map_comp0: thm,
   map_cong0: thm,

            (rel_conversepN, [Lazy.force (#rel_conversep 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)], []),
+           (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
            (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) =>