--- a/ProgTutorial/FirstSteps.thy	Mon Oct 12 17:07:17 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Oct 13 22:57:25 2009 +0200
@@ -1,8 +1,15 @@
 theory FirstSteps
 imports Base
-uses "FirstSteps.ML"
 begin
 
+(*<*)
+setup{*
+open_file_with_prelude 
+  "FirstSteps_Code.thy"
+  ["theory FirstSteps", "imports Main", "begin"]
+*}
+(*>*)
+
 chapter {* First Steps *}
 
 text {*
@@ -179,7 +186,8 @@
   You can print out error messages with the function @{ML_ind  error}; for 
   example:
 
-@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
+  @{ML_response_fake [display,gray] 
+  "if 0=1 then true else (error \"foo\")" 
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
@@ -1218,13 +1226,14 @@
 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
 
 text {* 
-  where each value needs to be given a default. To enable these values, they need to 
-  be set up with
+  where each value needs to be given a default. To enable these values on the 
+  user-level, they need to be set up with
 *}
 
 setup %gray {* 
   setup_bval #> 
-  setup_ival 
+  setup_ival #>
+  setup_sval
 *}
 
 text {*
@@ -1236,15 +1245,36 @@
 
 text {*
   On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}.
+  function @{ML_ind get in Config} from a proof context
+
+  @{ML_response [display,gray] 
+  "Config.get @{context} bval" 
+  "true"}
+
+  or from a theory using the function @{ML_ind get_thy in Config}
+
+  @{ML_response [display,gray] 
+  "Config.get_thy @{theory} bval" 
+  "true"}
 
-  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+  It is also possible to manipulate the configuration values
+  from the ML-level with the function @{ML_ind put in Config}
+  or @{ML_ind put_thy in Config}. For example
+
+  @{ML_response [display,gray]
+  "let
+  val ctxt = @{context}
+  val ctxt' = Config.put sval \"foo\" ctxt
+in
+  (Config.get ctxt sval, Config.get ctxt' sval)
+end"
+  "(\"some string\", \"foo\")"}
 
   \begin{readmore}
   For more information about configuration values see 
-  @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+  the files @{ML_file "Pure/Isar/attrib.ML"} and 
+  @{ML_file "Pure/config.ML"}.
   \end{readmore}
- 
 *}
 
 section {* Summary *}