src/Doc/Datatypes/Datatypes.thy

 \begin{enumerate}
 \setlength{\itemsep}{0pt}
 
 \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
 value.
 

     print_theorems
     print_bnfs
 
 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
 one generated by default is good enough, but in general this would be
 necessary. See \verb|~~/src/HOL/Basic_BNFs.thy|,