# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 46494c7dd344b9b35320eb63d18f2f03a816e0ff
# Parent  e78e7df36690f3dba673191dd1b40587e1dd0afd
added 'cong' attribute to 'map_cong'

diff -r e78e7df36690 -r 46494c7dd344 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -125,7 +125,7 @@
 open BNF_Tactics
 open BNF_Def_Tactics
 
-val fundef_cong_attrs = @{attributes [fundef_cong]};
+val cong_fundefcong_attrs = @{attributes [cong, fundef_cong]};
 
 type axioms = {
   map_id0: thm,
@@ -636,7 +636,7 @@
           val notes =
             [(map_compN, [Lazy.force (#map_comp facts)], []),
             (map_cong0N, [#map_cong0 axioms], []),
-            (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
+            (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
             (map_idN, [Lazy.force (#map_id facts)], []),
             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
             (rel_flipN, [Lazy.force (#rel_flip facts)], []),