diff -r a3be9a47e2d7 -r dcad9bad43e7 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 15:40:08 2014 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Nov 07 20:43:13 2014 +0100
@@ -1554,7 +1554,7 @@
 
 \item
 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
-@{keyword consts}.
+@{command consts}.
 
 \item
 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
@@ -2615,7 +2615,7 @@
 
 text {*
 \noindent
-Using \keyw{print_theorems} and @{keyword print_bnfs}, we can contemplate and
+Using \keyw{print_theorems} and @{command print_bnfs}, we can contemplate and
 show the world what we have achieved.
 
 This particular example does not need any nonemptiness witness, because the