--- a/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 21:29:25 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue May 03 21:40:14 2011 +0200
@@ -667,7 +667,7 @@
ML is augmented by special syntactic entities of the following form:
@{rail "
- @{syntax_def antiquote}: '@' '{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
+ @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
"}
Here @{syntax nameref} and @{syntax args} are regular outer syntax
--- 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}}}}[]