diff -r 01d7c4ba9050 -r 94f901e4969a doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:46:08 2010 +0100
@@ -320,9 +320,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}%
 \end{isamarkuptext}%
 \isamarkuptrue%