src/Doc/Isar_Ref/Outer_Syntax.thy

   content without delimiters.
 
   @{rail \<open>
     @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
       @{syntax ident} | @{syntax longident} | @{syntax symident} |
-      @{syntax nat}
+      @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat}
   \<close>}
 \<close>
 
 
 subsection \<open>Comments \label{sec:comments}\<close>

   symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well, provided
   these have not been superseded by commands or other keywords already (such
   as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
 
   @{rail \<open>
-    @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
-      @{syntax typevar}
-    ;
-    @{syntax_def term}: @{syntax embedded} | @{syntax var}
-    ;
-    @{syntax_def prop}: @{syntax term}
+    @{syntax_def type}: @{syntax embedded}
+    ;
+    @{syntax_def term}: @{syntax embedded}
+    ;
+    @{syntax_def prop}: @{syntax embedded}
   \<close>}
 
   Positional instantiations are specified as a sequence of terms, or the
   placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.