src/Doc/IsarImplementation/ML.thy

 text {* A very important consequence of embedding SML into Isar is the
   concept of \emph{ML antiquotation}.  The standard token language of
   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
   categories \cite{isabelle-isar-ref}.  Attributes and proof methods
   use similar syntax.