src/Doc/Datatypes/Datatypes.thy
changeset 60736 c4bc0691860b
parent 60301 ff82ba1893c8
child 60920 97c20589a0db
--- 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