--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 11 23:55:47 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 12 00:07:46 2013 +0200
@@ -408,9 +408,9 @@
discriminator associated with @{const Cons} is simply
@{term "\<lambda>xs. \<not> null xs"}.
-The @{text "defaults"} keyword following the @{const Nil} constructor specifies
-a default value for selectors associated with other constructors. Here, it is
-used to ensure that the tail of the empty list is itself (instead of being left
+The @{text defaults} clause following the @{const Nil} constructor specifies a
+default value for selectors associated with other constructors. Here, it is used
+to ensure that the tail of the empty list is itself (instead of being left
unspecified).
Because @{const Nil} is a nullary constructor, it is also possible to use