--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Sep 24 15:56:29 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Sep 24 16:17:59 2010 +0200
@@ -250,8 +250,8 @@
\item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
- \item @{text "@{type \<kappa>}"} prints a type constructor
- (logical or abbreviation) @{text "\<kappa>"}.
+ \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
+ constructor @{text "\<kappa>"}.
\item @{text "@{class c}"} prints a class @{text c}.