--- a/ProgTutorial/First_Steps.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue May 17 18:11:21 2011 +0100
@@ -537,22 +537,7 @@
   is often used for setup functions inside the
   \isacommand{setup}-command. These functions have to be of type @{ML_type
   "theory -> theory"}. More than one such setup function can be composed with
-  @{ML "#>"}. For example
-*}
-
-setup %gray {* let
-  val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1)
-  val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2)
-in
-  setup_ival1 #>
-  setup_ival2
-end *}
-
-text {*
-  after this the configuration values @{text ival1} and @{text ival2} are known
-  in the current theory and can be manipulated by the user (for more information 
-  about configuration values see Section~\ref{sec:storing}, for more about setup 
-  functions see Section~\ref{sec:theories}). 
+  @{ML "#>"}.\footnote{give example} 
   
   The remaining combinators we describe in this section add convenience for the
   ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
@@ -1308,22 +1293,12 @@
   values can be declared by
 *}
 
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" (K false)
-val (ival, setup_ival) = Attrib.config_int "ival" (K 0)
-val (sval, setup_sval) = Attrib.config_string "sval" (K "some string") *}
+ML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
+val ival = Attrib.setup_config_int @{binding "ival"} (K 0)
+val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *}
 
 text {* 
-  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_sval
-*}
-
-text {*
+  where each value needs to be given a default. 
   The user can now manipulate the values from the user-level of Isabelle 
   with the command
 *}