diff -r ae7707198403 -r e4c5c7ffceea doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue May 03 21:29:25 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue May 03 21:40:14 2011 +0200
@@ -799,8 +799,7 @@
   \begin{railoutput}
 \rail@begin{3}{\indexdef{}{syntax}{antiquote}\hypertarget{syntax.antiquote}{\hyperlink{syntax.antiquote}{\mbox{\isa{antiquote}}}}}
 \rail@bar
-\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[]
-\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
+\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
 \rail@nont{\isa{nameref}}[]
 \rail@nont{\isa{args}}[]
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]