--- a/ProgTutorial/Recipes/Antiquotes.thy	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue Jun 08 15:18:30 2010 +0200
@@ -35,7 +35,7 @@
 
   The code is checked by sending the ML-expression @{text [quotes] "val _ =
   a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
-  "ML_Context.eval_in"} in Line 4 below). The complete code of the
+  "ML_Context.eval_text_in"} in Line 4 below). The complete code of the
   document antiquotation is as follows:
 
 *}
@@ -43,10 +43,10 @@
 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml {context = ctxt, ...} code_txt =
-  (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
-   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
+  (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); 
+   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
+val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
 text {*
   The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
@@ -55,13 +55,13 @@
   function @{ML ml_val}, which constructs the appropriate ML-expression, and
   using @{ML "eval_in" in ML_Context}, which calls the compiler.  If the code is
   ``approved'' by the compiler, then the output function @{ML "output" in
-  ThyOutput} in the next line pretty prints the code. This function expects
+  Thy_Output} in the next line pretty prints the code. This function expects
   that the code is a list of (pretty)strings where each string correspond to a
   line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
   for txt} which produces such a list according to linebreaks.  There are a
   number of options for antiquotations that are observed by the function 
-  @{ML "output" in ThyOutput} when printing the code (including @{text "[display]"} 
-  and @{text "[quotes]"}). The function @{ML "antiquotation" in ThyOutput} in 
+  @{ML "output" in Thy_Output} when printing the code (including @{text "[display]"} 
+  and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in 
   Line 7 sets up the new document antiquotation.
 
   \begin{readmore}
@@ -74,10 +74,10 @@
 *}
 
 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
-  (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
-   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
+  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
+   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.antiquotation "ML_checked"
+val _ = Thy_Output.antiquotation "ML_checked"
          (Scan.lift (Parse.position Args.name)) output_ml *}
 
 text {*
@@ -128,15 +128,15 @@
 *}
 
 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 
-  (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
+  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
    let 
      val code_output = space_explode "\n" code_txt 
      val resp_output = add_resp (space_explode "\n" pat)
    in 
-     ThyOutput.output (map Pretty.str (code_output @ resp_output)) 
+     Thy_Output.output (map Pretty.str (code_output @ resp_output)) 
    end)
 
-val _ = ThyOutput.antiquotation "ML_resp" 
+val _ = Thy_Output.antiquotation "ML_resp" 
           (Scan.lift (Parse.position (Args.name -- Args.name))) 
              output_ml_resp*}