diff -r 76965c356d2a -r 2f8699695cf6 doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Wed Aug 18 09:46:59 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Wed Aug 18 09:55:00 2010 +0200
@@ -75,7 +75,7 @@
 end %quote
 
 text {*
-  After an interpretation of this locale (say, @{command
+  After an interpretation of this locale (say, @{command_def
   interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
   'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
   "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
@@ -131,7 +131,7 @@
 text {*
   Code generation may also be used to \emph{evaluate} expressions
   (using @{text SML} as target language of course).
-  For instance, the @{command value} reduces an expression to a
+  For instance, the @{command_def value} reduces an expression to a
   normal form with respect to the underlying code equations:
 *}