# HG changeset patch
# User wenzelm
# Date 1304451614 -7200
# Node ID e4c5c7ffceea3df4571def6004b5c4dfb5657f54
# Parent  ae7707198403a493d400675f2530e87e61ef1687
more precise syntax diagram;

diff -r ae7707198403 -r e4c5c7ffceea doc-src/IsarImplementation/Thy/ML.thy
--- 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
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}}}}[]