diff -r e3656cc81d27 -r 743020b817af ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Thu Nov 10 16:06:17 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 10 19:25:25 2011 +0000
@@ -201,7 +201,7 @@
   contain ``short-term memory data''. The reason is that a vast number of
   functions in Isabelle depend in one way or another on contexts. Even such
   mundane operations like printing out a term make essential use of contexts.
-  For this consider the following contrived proof-snippet whose only purpose is to 
+  For this consider the following contrived proof-snippet whose purpose is to 
   fix two variables:
 *}
 
@@ -218,7 +218,7 @@
 text {*
   The interesting point in this proof is that we injected ML-code before and after
   the variables are fixed. For this remember that ML-code inside a proof
-  needs to be enclosed in \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},
+  needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},
   not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function 
   @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes 
   a context and returns all its currently fixed variable (names). That 
@@ -227,7 +227,7 @@
   active at that point of the theory. Consequently, in the first call to 
   @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 
   filled with @{text x} and @{text y}. What is interesting is that contexts
-  can be stacked. For this consider the following proof fragment
+  can be stacked. For this consider the following proof fragment:
 *}
 
 lemma "True"
@@ -254,12 +254,15 @@
 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}
 
 text {*
-  Now let us come back to the point about printing terms.
+  where the function @{ML_ind add_fixes in Variable} fixes a list of variables
+  specified by strings. Let us come back to the point about printing terms. Consider
+  printing out the term @{text "(x, y, z, w)"} using the function @{ML_ind pretty_term}.
+  This function takes a term and a context as argument. 
 *}
 
 ML {*
 let
-  val trm = @{term "x y z w"}
+  val trm = @{term "(x, y, z, w)"}
 in
   pwriteln (Pretty.chunks 
     [ pretty_term ctxt0 trm,
@@ -270,7 +273,21 @@
 
 
 text {*
-  
+  The term we are printing is in all three cases the same---a tuple containing four
+  free variables. As you can see in case of @{ML "ctxt0"}, however, all variables are highlighted 
+  indicating a problem, while in case of @{ML "ctxt1"} @{text x} and @{text y} are printed
+  as normal (blue) free variables, but not @{text z} and @{text w}. In the last case all 
+  variables are printed as expected. The point is that the context contains the information 
+  which variables are fixed, and designates all other free variables as being alien or faulty.
+  While this seems like a minor feat, the concept of making the context aware of 
+  fixed variables is actually quite useful. For example it prevents us from fixing a 
+  variable twice
+
+  @{ML_response_fake [gray, display]
+  "@{context}
+|> Variable.add_fixes [\"x\", \"y\"] 
+||>> Variable.add_fixes [\"x\", \"y\"]" 
+  "Duplicate fixed variable(s): \"x\""}
 *}