diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Recipes/Config.thy
--- a/CookBook/Recipes/Config.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -12,8 +12,8 @@
 
   {\bf Solution:} This can be achieved using configuration values.\smallskip
 
-  Assume you want to control three values, namely @{ML_text bval} containing a
-  boolean,  @{ML_text ival} containing an integer and @{ML_text sval} 
+  Assume you want to control three values, namely @{text bval} containing a
+  boolean,  @{text ival} containing an integer and @{text sval} 
   containing a string. These values can be declared on the ML-level with
 *}