--- a/src/Doc/Datatypes/Datatypes.thy Fri Feb 07 00:19:02 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Feb 07 00:48:04 2014 +0100
@@ -1847,8 +1847,12 @@
text {*
This generates the lemma collection @{thm [source] lappend_simps}:
%
-\[@{thm lappend_simps(1)[no_vars]}
- \qquad @{thm lappend_simps(2)[no_vars]}\]
+\begin{gather*%
+}
+ @{thm lappend_simps(1)[no_vars]} \\
+ @{thm lappend_simps(2)[no_vars]}
+\end{gather*%
+}
%
Corecursion is useful to specify not only functions but also infinite objects:
*}