diff -r 1266b6208a5b -r 4e7ddd76e632 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 15:36:54 2013 +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 '}'
   "}
 
   Here @{syntax nameref} and @{syntax args} are regular outer syntax