1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:43:49 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:46:08 2010 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5      altname: '(' (name | 'open' | 'open' name) ')'
     1.6      ;
     1.7 -    abstype: typespec mixfix?
     1.8 +    abstype: typespecsorts mixfix?
     1.9      ;
    1.10      repset: term ('morphisms' name name)?
    1.11      ;

     2.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:43:49 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:46:08 2010 +0100
     2.3 @@ -297,9 +297,13 @@
     2.4    only plain postfix notation is available here, but no infixes.
     2.5  
     2.6    \indexouternonterm{typespec}
     2.7 +  \indexouternonterm{typespecsorts}
     2.8    \begin{rail}
     2.9      typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
    2.10      ;
    2.11 +
    2.12 +    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
    2.13 +    ;
    2.14    \end{rail}
    2.15  *}
    2.16  

     3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:43:49 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:46:08 2010 +0100
     3.3 @@ -37,7 +37,7 @@
     3.4  
     3.5      altname: '(' (name | 'open' | 'open' name) ')'
     3.6      ;
     3.7 -    abstype: typespec mixfix?
     3.8 +    abstype: typespecsorts mixfix?
     3.9      ;
    3.10      repset: term ('morphisms' name name)?
    3.11      ;

     4.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:43:49 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:46:08 2010 +0100
     4.3 @@ -320,9 +320,13 @@
     4.4    only plain postfix notation is available here, but no infixes.
     4.5  
     4.6    \indexouternonterm{typespec}
     4.7 +  \indexouternonterm{typespecsorts}
     4.8    \begin{rail}
     4.9      typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
    4.10      ;
    4.11 +
    4.12 +    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
    4.13 +    ;
    4.14    \end{rail}%
    4.15  \end{isamarkuptext}%
    4.16  \isamarkuptrue%