--- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 15 00:21:32 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 15 00:35:07 2014 +0200
@@ -886,8 +886,9 @@
@{thm list.rel_intros(1)[no_vars]} \\
@{thm list.rel_intros(2)[no_vars]}
-\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
-@{thm list.rel_cases[no_vars]}
+% FIXME (and add @ before antiquotation below)
+%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
+%{thm list.rel_cases[no_vars]}
\end{description}
\end{indentblock}