--- a/ProgTutorial/Advanced.thy	Sat Nov 12 11:45:39 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Sat Nov 12 20:28:30 2011 +0000
@@ -295,10 +295,10 @@
   variables, but not @{text z} and @{text w}. In the last case all variables
   are printed as expected. The point of this example 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
-  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
+  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
 
   @{ML_response_fake [gray, display]
   "@{context}
@@ -371,8 +371,40 @@
 end"
   "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
 
-  The most useful feature of contexts is that one can export, for example,
-  terms between contexts.
+  The most useful feature of contexts is that one can export terms and theorems 
+  between contexts. Let us consider first the case of terms. 
+
+  \begin{isabelle}
+  \begin{graybox}
+  \begin{linenos}
+  @{ML "let
+  val ctxt0 = @{context}
+  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 ctxt0
+  |> pwriteln
+end"}
+  \end{linenos}
+  \setlength{\fboxsep}{0mm}
+  @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
+  @{text "?x ?y ?z"}
+  \end{graybox}
+  \end{isabelle}
+
+  In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in context @{text ctxt1}.
+  The function @{ML_ind export_terms in Variable} from the @{ML_struct Variable} can be used 
+  to ``transfer'' terms between contexts. Transferring means to turn all (free) variables that
+  are fixed in one context, but not in the other, into schematic variables. In our example
+  we are transferring the term @{text "P x y z"} from context @{text "ctxt1"} into @{text "ctxt0"}
+  which means @{term x}, @{term y} and @{term z} become schematic variables (as can be seen 
+  by the leading question mark). Note that the variable @{text P} stays a free variable, since 
+  it not fixed in @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does not
+  know about it. Note also that in Line 6 we had to use the function @{ML_ind singleton}, 
+  because the function @{ML_ind export_terms in Variable} normally works over lists of terms.
+  
+  
 *}
 
 ML {*