# HG changeset patch
# User desharna
# Date 1409570580 -7200
# Node ID 73f46283c247767186cd3bf0415d5851ed1fa8a2
# Parent  e7ebe555428137d03a2dd3e6cabb31c0668ec942
note 'map_transfer' more often

diff -r e7ebe5554281 -r 73f46283c247 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Aug 31 09:10:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Sep 01 13:23:00 2014 +0200
@@ -676,7 +676,6 @@
            (in_monoN, [Lazy.force (#in_mono facts)]),
            (in_relN, [Lazy.force (#in_rel facts)]),
            (map_comp0N, [#map_comp0 axioms]),
-           (map_transferN, [Lazy.force (#map_transfer facts)]),
            (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
            (set_map0N, #set_map0 axioms),
@@ -700,6 +699,7 @@
            (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
            (map_idN, [Lazy.force (#map_id facts)], []),
            (map_id0N, [#map_id0 axioms], []),
+           (map_transferN, [Lazy.force (#map_transfer facts)], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),