# HG changeset patch
# User desharna
# Date 1408362587 -7200
# Node ID 1e7b9579b14fc50d2cb832f35943177defea97dc
# Parent  00e9c6d367e7b50f5bf049799ea80132faba4683
note 'inj_map' more often

diff -r 00e9c6d367e7 -r 1e7b9579b14f src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 13:46:26 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 13:49:47 2014 +0200
@@ -913,6 +913,9 @@
 \begin{indentblock}
 \begin{description}
 
+\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
+@{thm list.inj_map[no_vars]}
+
 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
 @{thm list.set_map[no_vars]}
 
diff -r 00e9c6d367e7 -r 1e7b9579b14f src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:49:47 2014 +0200
@@ -659,7 +659,6 @@
            (in_bdN, [Lazy.force (#in_bd facts)]),
            (in_monoN, [Lazy.force (#in_mono facts)]),
            (in_relN, [Lazy.force (#in_rel facts)]),
-           (inj_mapN, [Lazy.force (#inj_map facts)]),
            (map_comp0N, [#map_comp0 axioms]),
            (map_transferN, [Lazy.force (#map_transfer facts)]),
            (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
@@ -677,7 +676,8 @@
     fun note_unless_dont_note (noted0, lthy0) =
       let
         val notes =
-          [(map_compN, [Lazy.force (#map_comp facts)], []),
+          [(inj_mapN, [Lazy.force (#inj_map facts)], []),
+           (map_compN, [Lazy.force (#map_comp facts)], []),
            (map_cong0N, [#map_cong0 axioms], []),
            (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
            (map_idN, [Lazy.force (#map_id facts)], []),