--- 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]}
--- 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)], []),