--- a/ProgTutorial/Advanced.thy	Fri Nov 11 16:27:04 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Sat Nov 12 11:45:39 2011 +0000
@@ -216,7 +216,7 @@
   txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
 
 text {*
-  The interesting point in this proof is that we injected ML-code before and after
+  The interesting point 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 inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},
   not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function 
@@ -247,7 +247,7 @@
   the second time we get only the fixes variables @{text x} and @{text y} as answer, since
   @{text z} and @{text w} are not anymore in the scope of the context. 
   This means the curly-braces act on the Isabelle level as opening and closing statements 
-  for a context. The above proof fragment corresoponds roughly to the following ML-code
+  for a context. The above proof fragment corresponds roughly to the following ML-code
 *}
 
 ML{*val ctxt0 = @{context};
@@ -258,7 +258,8 @@
   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 \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}.
-  This function takes a term and a context as argument. 
+  This function takes a term and a context as argument. Notice how the printing
+  of the term changes with which context is used.
 
   \begin{isabelle}
   \begin{graybox}
@@ -288,7 +289,7 @@
 
 
   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
+  four free variables. As you can see, however, in case of @{ML "ctxt0"} 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
@@ -304,8 +305,8 @@
 |> Variable.add_fixes [\"x\", \"x\"]" 
   "ERROR: Duplicate fixed variable(s): \"x\""}
 
-  But it also allows us to easily create fresh free variables avoiding any 
-  clashes. In Line~3 below we fix the variable @{text x} in the context
+  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"}.
 
@@ -321,12 +322,12 @@
   "([(\"x\", \"nat\"), (\"xa\", \"nat\")], 
  [(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
 
-  As can be seen, if we create the fresh variables with the context @{text ctxt0},
+  As you can see, if we create the fresh variables with the context @{text ctxt0},
   then we obtain @{text "x"} and @{text "xa"}; but in @{text ctxt1} we obtain @{text "xa"}
   and @{text "xb"} avoiding @{text x}, which was fixed in this context.
 
-  Often one has the situation that given some terms, create fresh variables
-  avoiding any variable occuring in those terms. For this you can use the
+  Often one has the problem that given some terms, create fresh variables
+  avoiding any variable occurring in those terms. For this you can use the
   function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}.
 
   @{ML_response_fake [gray, display]
@@ -338,10 +339,11 @@
 end"
   "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
 
-  The result is @{text xb} and @{text xc} for the names of the freshh variables. This 
-  is also important when parsing terms, for example with the function 
-  @{ML_ind read_term in Syntax} from the structure @{ML_struct Syntax}. Consider 
-  the following code:
+  The result is @{text xb} and @{text xc} for the names of the fresh
+  variables. Note that @{ML_ind declare_term in Variable} does not fix the
+  variables; it just makes them ``known'' to the context. This is helpful when
+  parsing terms using the function @{ML_ind read_term in Syntax} from the
+  structure @{ML_struct Syntax}. Consider the following code:
 
   @{ML_response_fake [gray, display]
   "let
@@ -353,11 +355,11 @@
 end"
   "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
   
-  Parsing the string in the first context results in a free variable 
-  with a default polymorphic type, but in the second case we obtain a
+  Parsing the string in the context @{text "ctxt0"} results in a free variable 
+  with a default polymorphic type, but in case of @{text "ctxt1"} we obtain a
   free variable of type @{typ nat} as previously declared. Which
-  type the parsed term receives depends on the last declaration that
-  is made as the next example illustrates.
+  type the parsed term receives depends upon the last declaration that
+  is made, as the next example illustrates.
 
   @{ML_response_fake [gray, display]
   "let
@@ -369,14 +371,39 @@
 end"
   "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
 
+  The most useful feature of contexts is that one can export, for example,
+  terms between contexts.
 *}
 
 ML {*
 let
   val ctxt0 = @{context}
-  val trm = @{prop "P x y z"}
-  val foo_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt0) trm
   val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
+  val foo_trm = @{term "P x y z"}
+in
+  singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
+  |> pretty_term ctxt1
+  |> pwriteln
+end
+*}
+
+ML {*
+let
+  val thy = @{theory}
+  val ctxt0 = @{context}
+  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
+  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
+in
+  singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
+end
+*}
+
+ML {*
+let
+  val thy = @{theory}
+  val ctxt0 = @{context}
+  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
+  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
 in
   singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
 end

--- a/ProgTutorial/First_Steps.thy	Fri Nov 11 16:27:04 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Sat Nov 12 11:45:39 2011 +0000
@@ -669,13 +669,13 @@
 
 ML{*val (((one_def, two_def), three_def), ctxt') = 
   @{context}
-  |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
+  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
 
 text {*
-  where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
-  and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
+  where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"}
+  and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial
   context with the definitions. The result we are interested in is the
   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 
   information about the definitions---the function @{ML_ind add_def in Local_Defs} returns

Binary file progtutorial.pdf has changed