diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Sun May 01 00:01:59 2011 +0200
@@ -81,10 +81,12 @@
   @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
-  ;
-  \end{rail}
+  @{rail "
+  (@@{ML_antiquotation class_syntax} |
+   @@{ML_antiquotation type_syntax} |
+   @@{ML_antiquotation const_syntax} |
+   @@{ML_antiquotation syntax_const}) name
+  "}
 
   \begin{description}