src/Doc/Datatypes/Datatypes.thy

 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]} \\
 (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]}
 
 \end{description}

 @{thm list.size(1)[no_vars]} \\
 @{thm list.size(2)[no_vars]} \\
 @{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]}
 
 \end{description}
 \end{indentblock}