--- a/ProgTutorial/Recipes/Config.thy	Thu Mar 19 17:50:28 2009 +0100
+++ b/ProgTutorial/Recipes/Config.thy	Thu Mar 19 23:21:26 2009 +0100
@@ -4,7 +4,6 @@
 
 section {* Configuration Options\label{rec:config} *} 
 
-
 text {*
   {\bf Problem:} 
   You would like to enhance your tool with options that can be changed 
@@ -29,7 +28,7 @@
 setup {* setup_bval *} 
 setup {* setup_ival *}
 
-text {* or on the ML-level *}
+text {* or on the ML-level with *}
 
 ML{*setup_sval @{theory} *}
 
@@ -57,7 +56,7 @@
 setup {* Config.put_thy sval "bar" *}
 
 text {* 
-  Now the retrival of this value yields:
+  Now the retrieval of this value yields:
 
   @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
 
@@ -66,9 +65,9 @@
 
   @{ML_response [display,gray] 
 "let 
-  val ctxt = Config.map ival (fn i => i + 1) @{context}
+  val ctxt' = Config.map ival (fn i => i + 1) @{context}
 in 
-  Config.get ctxt ival
+  Config.get ctxt' ival
 end" "4"}
 
   \begin{readmore}
@@ -76,8 +75,8 @@
   \end{readmore}
 
   There are many good reasons to control parameters in this way. One is
-  that it avoid global references, which cause many headaches with the
-  multithreaded execution of Isabelle.
-  
-  *}
+  that no global reference is needed, which would cause many headaches 
+  with the multithreaded execution of Isabelle.
+*}
+
 end
\ No newline at end of file