--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:11 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:12 2014 +0200
@@ -1021,6 +1021,9 @@
(The @{text "[code]"} attribute is set by the @{text code} plugin,
Section~\ref{ssec:code-generator}.)
+\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
@{thm list.rec_transfer[no_vars]}
@@ -2860,9 +2863,6 @@
@{thm list.size(3)[no_vars]} \\
@{thm list.size(4)[no_vars]}
-\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
-@{thm list.rec_o_map[no_vars]}
-
\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
@{thm list.size_o_map[no_vars]}