--- a/ProgTutorial/Advanced.thy	Fri Nov 04 09:29:50 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Sat Nov 05 18:44:28 2011 +0000
@@ -73,22 +73,26 @@
 section {* Setups (TBD) *}
 
 text {*
-  In the previous section we used \isacommand{setup}, for example, in
-  order to make a theorem attribute known to Isabelle. What happens
-  behind the scenes is that \isacommand{setup} expects a function of
-  type @{ML_type "theory -> theory"}: the input theory is the current
-  theory and the output the theory where the theory attribute has been
+  In the previous section we used \isacommand{setup} in order, for example, 
+  to make a theorem attribute known to Isabelle or register a theorem under
+  a name. What happens behind the scenes is that \isacommand{setup} expects a 
+  function of type @{ML_type "theory -> theory"}: the input theory is the current
+  theory and the output the theory where the theory attribute or theorem has been
   stored.
 
   This is a fundamental principle in Isabelle. A similar situation arises
   with declaring constants. The function that declares a 
   constant on the ML-level is @{ML_ind  declare_const in Sign}. 
-  However, if you simply write\footnote{Recall that ML-code  needs to be 
+  However, note that if you simply write\footnote{Recall that ML-code  needs to be 
   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
 *}  
 
-ML{*Sign.declare_const @{context} 
-  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) @{theory} *}
+ML{*let
+  val thy = @{theory}
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
+in 
+  Sign.declare_const @{context} bar_const thy  
+end*}
 
 text {*
   with the intention of declaring the constant @{text "BAR"} with type @{typ nat} 
@@ -96,22 +100,25 @@
   query the constant on the Isabelle level using the command \isacommand{term}
 
   \begin{isabelle}
-  \isacommand{term}~@{text [quotes] "BAR"}\\
+  \isacommand{term}~@{text BAR}\\
   @{text "> \"BAR\" :: \"'a\""}
   \end{isabelle}
 
-  you can see that you do not obtain a constant of type @{typ nat}, but a free 
+  you can see that you do \emph{not} obtain a constant of type @{typ nat}, but a free 
   variable (printed in blue) of polymorphic type. The problem is that the 
   ML-expression above did not ``register'' the declaration with the current theory. 
   This is what the command \isacommand{setup} is for. The constant is properly 
   declared with
 *}
 
-setup %gray {* Sign.declare_const @{context} 
-  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) #> snd *}
+setup %gray {* let
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
+in 
+  Sign.declare_const @{context} bar_const #> snd 
+end *}
 
 text {* 
-  Now 
+  where the declaration is actually applied to the theory and
   
   \begin{isabelle}
   \isacommand{term}~@{text [quotes] "BAR"}\\
@@ -120,6 +127,12 @@
 
   returns a (black) constant with the type @{typ nat}, as expected.
 
+  In a sense, \isacommand{setup} can be seen as a transaction that takes the
+  current theory, applies an operation, and produces a new current theory. This
+  means that we have to be careful to apply operations always to the current
+  theory, not to a \emph{stale} one. The code below produces
+
+
   A similar command is \isacommand{local\_setup}, which expects a function
   of type @{ML_type "local_theory -> local_theory"}. Later on we will also
   use the commands \isacommand{method\_setup} for installing methods in the