doc-src/IsarRef/Thy/Outer_Syntax.thy

--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:46:08 2010 +0100
@@ -297,9 +297,13 @@
   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}
 *}