document 'rec_transfer'

--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 16:35:53 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 16:35:54 2014 +0200
@@ -1014,6 +1014,9 @@
 (The @{text "[code]"} attribute is set by the @{text code} plugin,
 Section~\ref{ssec:code-generator}.)
 
+\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
+@{thm list.rec_transfer[no_vars]}
+
 \end{description}
 \end{indentblock}