# HG changeset patch
# User wenzelm
# Date 1268955968 -3600
# Node ID 94f901e4969a402b7ad9022afbc0fe15cbad4c5b
# Parent  01d7c4ba9050475e32b4047f9b35c2d74271fad3
allow sort constraints in HOL/typedef;

diff -r 01d7c4ba9050 -r 94f901e4969a doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:46:08 2010 +0100
@@ -17,7 +17,7 @@
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec mixfix?
+    abstype: typespecsorts mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
diff -r 01d7c4ba9050 -r 94f901e4969a 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}
 *}
 
diff -r 01d7c4ba9050 -r 94f901e4969a doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:46:08 2010 +0100
@@ -37,7 +37,7 @@
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec mixfix?
+    abstype: typespecsorts mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
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%