--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 20:59:24 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue May 03 21:07:24 2011 +0200
@@ -849,7 +849,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[]
\rail@plus
\rail@plus
@@ -863,7 +863,7 @@
\rail@cterm{\isa{\isakeyword{and}}}[]
\rail@endplus
\rail@end
-\rail@begin{3}{\isa{}}
+\rail@begin{3}{}
\rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[]
\rail@plus
\rail@bar