--- 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}}}}[]