--- a/ProgTutorial/Advanced.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue May 17 18:11:21 2011 +0100
@@ -127,8 +127,8 @@
 
 section {* Contexts (TBD) *}
 
-ML_command "ProofContext.debug := true"
-ML_command "ProofContext.verbose := true"
+ML{*ProofContext.debug*}
+ML{*ProofContext.verbose*}
 
 
 section {* Local Theories (TBD) *}
@@ -276,14 +276,9 @@
   section and link with the comment in the antiquotation section.}
 
   Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or
-  @{ML_ind  Long_Name.base_name}. For example:
+  constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
-
-  The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
-  strips off all qualifiers.
+  @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
 
   \begin{readmore}
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

--- a/ProgTutorial/Base.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/Base.thy	Tue May 17 18:11:21 2011 +0100
@@ -15,10 +15,9 @@
 (* they also write the code into a separate file  *)
 
 ML {*
-val (filename, setup_filename) = Attrib.config_string "filename" (K "File_Code.ML")
+val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML")
 *}
 
-setup {* setup_filename *}
 
 ML {*
 fun write_file txt thy =

--- 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
 *}

--- a/ProgTutorial/Intro.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/Intro.thy	Tue May 17 18:11:21 2011 +0100
@@ -290,7 +290,7 @@
   
   This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\
   \input{version}\\
-  \input{pversion}
+  %%\input{pversion}
 *}
 
 end

Binary file progtutorial.pdf has changed