doc-src/IsarRef/Thy/document/Outer_Syntax.tex

   \railnonterm{typespec} on the 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.
 
   \indexouternonterm{typespec}
+  \indexouternonterm{typespecsorts}
   \begin{rail}
     typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
+    ;
+
+    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
     ;
   \end{rail}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %