--- a/ProgTutorial/First_Steps.thy	Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/First_Steps.thy	Fri Oct 29 11:00:37 2010 +0100
@@ -259,17 +259,17 @@
 
 text {*
   You can also print out terms together with their typing information.
-  For this you need to set the reference @{ML_ind show_types in Syntax} 
-  to @{ML true}.
+  For this you need to set the configuration value 
+  @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 
-ML{*show_types := true*}
+ML{*val show_types_ctxt = Config.put show_types true @{context}*}
 
 text {*
-  Now @{ML pretty_term} prints out
+  Now by using this context @{ML pretty_term} prints out
 
   @{ML_response_fake [display, gray]
-  "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
+  "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
   "(1::nat, x::'a)"}
 
   where @{text 1} and @{text x} are displayed with their inferred type.
@@ -277,19 +277,18 @@
   the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
   In this case we obtain
 *}
-(*<*)ML %linenos {*show_all_types := true*}
-(*>*)
+
 text {*
   @{ML_response_fake [display, gray]
-  "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
+  "pwriteln (pretty_term 
+  (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})"
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
   where @{term Pair} is the term-constructor for products. 
-  Other references that influence printing of terms are 
+  Other configuration values that influence printing of terms are 
   @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. 
 *}
-(*<*)ML %linenos {*show_types := false; show_all_types := false*}
-(*>*)
+
 text {*
   A @{ML_type cterm} can be printed with the following function.
 *}