# HG changeset patch
# User wenzelm
# Date 1271357764 -7200
# Node ID d2ad76e374d3a86c1a6478321a63322052a23910
# Parent  2fb3e278a5d7282d78d13eed881a62c564d76978
HOL record: explicitly allow sort constraints;

diff -r 2fb3e278a5d7 -r d2ad76e374d3 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Apr 15 20:37:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Apr 15 20:56:04 2010 +0200
@@ -178,7 +178,7 @@
   \end{matharray}
 
   \begin{rail}
-    'record' typespec '=' (type '+')? (constdecl +)
+    'record' typespecsorts '=' (type '+')? (constdecl +)
     ;
   \end{rail}
 
diff -r 2fb3e278a5d7 -r d2ad76e374d3 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Apr 15 20:37:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Apr 15 20:56:04 2010 +0200
@@ -202,7 +202,7 @@
   \end{matharray}
 
   \begin{rail}
-    'record' typespec '=' (type '+')? (constdecl +)
+    'record' typespecsorts '=' (type '+')? (constdecl +)
     ;
   \end{rail}