src/Doc/Isar_Ref/Outer_Syntax.thy

   left-hand side. This models basic type constructor application at the outer
   syntax level. Note that only plain postfix notation is available here, but
   no infixes.
 
   \<^rail>\<open>
-    @{syntax_def typespec}:
-      (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name}
-    ;
-    @{syntax_def typespec_sorts}:
+    @{syntax_def typeargs}:
+      (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')')
+    ;
+    @{syntax_def typeargs_sorts}:
       (() | (@{syntax type_ident} ('::' @{syntax sort})?) |
-        '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
+        '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')')
+    ;
+    @{syntax_def typespec}: @{syntax typeargs} @{syntax name}
+    ;
+    @{syntax_def typespec_sorts}: @{syntax typeargs_sorts} @{syntax name}
   \<close>
 \<close>
 
 
 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>