--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 29 10:39:39 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 29 10:39:39 2014 +0200
@@ -900,9 +900,8 @@
@{thm list.rel_intros(1)[no_vars]} \\
@{thm list.rel_intros(2)[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]}
+\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]}
\item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
@{thm list.rel_sel[no_vars]}