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