diff -r 6f37a300c82b -r 117c5d2c2642 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 29 14:21:24 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 29 14:21:25 2014 +0200
@@ -856,6 +856,9 @@
 \begin{indentblock}
 \begin{description}
 
+\item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\
+@{thm list.case_transfer[no_vars]}
+
 \item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\
 @{thm list.ctr_transfer(1)[no_vars]} \\
 @{thm list.ctr_transfer(2)[no_vars]}