--- a/ProgTutorial/Advanced.thy	Wed Nov 16 13:23:27 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 17 12:20:19 2011 +0000
@@ -298,17 +298,28 @@
   free variables as being alien or faulty.  Therefore the highlighting. 
   While this seems like a minor detail, the concept of making the context aware 
   of fixed variables is actually quite useful. For example it prevents us from 
-  fixing a variable twice.
+  fixing a variable twice
 
   @{ML_response_fake [gray, display]
   "@{context}
 |> Variable.add_fixes [\"x\", \"x\"]" 
   "ERROR: Duplicate fixed variable(s): \"x\""}
 
-  More importantly it also allows us to easily create fresh free variables avoiding any 
-  clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context
-  @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat}
-  as variants of the string @{text [quotes] "x"} (Lines 6 and 7).
+  More importantly it also allows us to easily create fresh names for
+  fixed variables.  For this you have to use the function @{ML_ind
+  variant_fixes in Variable} from the structure @{ML_struct Variable}.
+
+  @{ML_response_fake [gray, display]
+  "@{context}
+|> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 
+  "([\"y\", \"ya\", \"z\"], ...)"}
+
+  Now a fresh variant for the second occurence of @{text y} is created
+  avoiding any clash. In this way we can also create free variables
+  that avoid any clashes with fixed variables. In Line~3 below we fix
+  the variable @{text x} in the context @{text ctxt1}. Next we want to
+  create two fresh variables of type @{typ nat} as variants of the
+  string @{text [quotes] "x"} (Lines 6 and 7).
 
   @{ML_response_fake [display, gray, linenos]
   "let
@@ -448,9 +459,9 @@
 end"
   "?P ?x ?y ?z ?x ?y ?z"}
 
-  Since we fixed all variables in @{text ctxt1}, in result all of them 
-  are schematic. The great point is that exporting between contexts is 
-  not just concerned with variables, but also assumptions. For this we
+  Since we fixed all variables in @{text ctxt1}, in the result all of them 
+  are schematic. The great point of contexts is that exporting from one to 
+  another is not just concerned with variables, but also assumptions. For this we
   can use the function @{ML_ind export in Assumption} from the structure
   @{ML_struct Assumption}. Consider the following code.
 

Binary file progtutorial.pdf has changed