--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 15 16:11:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 15 16:14:14 2014 +0200
@@ -152,6 +152,7 @@
open BNF_Def_Tactics
val fundefcong_attrs = @{attributes [fundef_cong]};
+val mono_attrs = @{attributes [mono]};
type axioms = {
map_id0: thm,
@@ -730,7 +731,7 @@
(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), [])]