--- a/ProgTutorial/Recipes/Antiquotes.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -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_text_in"} in Line 4 below). The complete code of the
+  "ML_Context.eval_source_in"} in Line 7 below). The complete code of the
   document antiquotation is as follows:
 
 *}
@@ -43,8 +43,12 @@
 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml {context = ctxt, ...} code_txt =
-  (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); 
+let
+  val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none}
+in
+  (ML_Context.eval_source_in (SOME ctxt) false srcpos; 
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
+end
 
 val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*}
 
@@ -76,8 +80,12 @@
 *}
 
 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
-  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
+let
+  val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}
+in
+  (ML_Context.eval_source_in (SOME ctxt) false srcpos;
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
+end
 
 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}
          (Scan.lift (Parse.position Args.name)) output_ml *}
@@ -132,7 +140,11 @@
 *}
 
 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 
-  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
+  (let
+     val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}
+   in
+     ML_Context.eval_source_in (SOME ctxt) false srcpos 
+   end;
    let 
      val code_output = space_explode "\n" code_txt 
      val resp_output = add_resp (space_explode "\n" pat)
@@ -140,6 +152,7 @@
      Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 
    end)
 
+
 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} 
           (Scan.lift (Parse.position (Args.name -- Args.name))) 
              output_ml_resp*}