diff -r 824d3f1d8de6 -r 2080fe35abea doc-src/IsarImplementation/Thy/document/ML.tex
--- 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