298   free variables as being alien or faulty.  While this seems like a minor

   298   free variables as being alien or faulty.  Therefore the highlighting. 

   299   detail, the concept of making the context aware of fixed variables is

   299   While this seems like a minor detail, the concept of making the context aware 

   300   actually quite useful. For example it prevents us from fixing a variable

   300   of fixed variables is actually quite useful. For example it prevents us from 

   301   twice

   301   fixing a variable twice

   374   The most useful feature of contexts is that one can export, for example,

   374   The most useful feature of contexts is that one can export terms and theorems 

   375   terms between contexts.

   375   between contexts. Let us consider first the case of terms. 

   376 

   377   \begin{isabelle}

   378   \begin{graybox}

   379   \begin{linenos}

   380   @{ML "let

   381   val ctxt0 = @{context}

   382   val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 

   383   val foo_trm = @{term \"P x y z\"}

   384 in

   385   singleton (Variable.export_terms ctxt1 ctxt0) foo_trm

   386   |> pretty_term ctxt0

   387   |> pwriteln

   388 end"}

   389   \end{linenos}

   390   \setlength{\fboxsep}{0mm}

   391   @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%

   392   @{text "?x ?y ?z"}

   393   \end{graybox}

   394   \end{isabelle}

   395 

   396   In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in context @{text ctxt1}.

   397   The function @{ML_ind export_terms in Variable} from the @{ML_struct Variable} can be used 

   398   to ``transfer'' terms between contexts. Transferring means to turn all (free) variables that

   399   are fixed in one context, but not in the other, into schematic variables. In our example

   400   we are transferring the term @{text "P x y z"} from context @{text "ctxt1"} into @{text "ctxt0"}

   401   which means @{term x}, @{term y} and @{term z} become schematic variables (as can be seen 

   402   by the leading question mark). Note that the variable @{text P} stays a free variable, since 

   403   it not fixed in @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does not

   404   know about it. Note also that in Line 6 we had to use the function @{ML_ind singleton}, 

   405   because the function @{ML_ind export_terms in Variable} normally works over lists of terms.

   406   

   407