# HG changeset patch
# User traytel
# Date 1418303679 -3600
# Node ID 347fece4a85ec3719a31ee4eca88ed0b3b22c892
# Parent  f2819313e3cc35e39cd04eb0077cec68f091aa1b
note more facts (always)

diff -r f2819313e3cc -r 347fece4a85e src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Dec 11 14:14:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Dec 11 14:14:39 2014 +0100
@@ -697,10 +697,8 @@
            (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)
@@ -714,7 +712,8 @@
     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], []),
@@ -732,6 +731,7 @@
            (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), [])]