# HG changeset patch
# User blanchet
# Date 1437060344 -7200
# Node ID c4bc0691860b79f39c21344b53633ce8d8859fcb
# Parent  cf291b55f3d163a86d294245f12f9a23ef0a83e1
generalized limitation in documentation

diff -r cf291b55f3d1 -r c4bc0691860b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:25:44 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:25:44 2015 +0200
@@ -3186,8 +3186,8 @@
 processed more efficiently.
 
 \item
-\emph{Locally fixed types cannot be used in (co)datatype specifications.}
-This limitation can be circumvented by adding type arguments to the local
+\emph{Locally fixed types and terms cannot be used in type specifications.}
+The limitation on types can be circumvented by adding type arguments to the local
 (co)datatypes to abstract over the locally fixed types.
 
 \item