src/Doc/Isar_Ref/Outer_Syntax.thy

   admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
   text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
   Isabelle/Isar commands.
 
   @{rail \<open>
-    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
+    @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
     ;
     @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
   \<close>}
 \<close>