src/HOL/Tools/BNF/bnf_def.ML
changeset 57969 1e7b9579b14f
parent 57968 00e9c6d367e7
child 57970 eaa986cd285a
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:49:47 2014 +0200
     1.3 @@ -659,7 +659,6 @@
     1.4             (in_bdN, [Lazy.force (#in_bd facts)]),
     1.5             (in_monoN, [Lazy.force (#in_mono facts)]),
     1.6             (in_relN, [Lazy.force (#in_rel facts)]),
     1.7 -           (inj_mapN, [Lazy.force (#inj_map facts)]),
     1.8             (map_comp0N, [#map_comp0 axioms]),
     1.9             (map_transferN, [Lazy.force (#map_transfer facts)]),
    1.10             (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
    1.11 @@ -677,7 +676,8 @@
    1.12      fun note_unless_dont_note (noted0, lthy0) =
    1.13        let
    1.14          val notes =
    1.15 -          [(map_compN, [Lazy.force (#map_comp facts)], []),
    1.16 +          [(inj_mapN, [Lazy.force (#inj_map facts)], []),
    1.17 +           (map_compN, [Lazy.force (#map_comp facts)], []),
    1.18             (map_cong0N, [#map_cong0 axioms], []),
    1.19             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    1.20             (map_idN, [Lazy.force (#map_id facts)], []),