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)?
     ;