--- a/ProgTutorial/Recipes/Antiquotes.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue May 21 16:22:30 2019 +0200
@@ -40,7 +40,7 @@
 \<close>
 ML \<open>Input.pos_of\<close>
 ML%linenosgray\<open>fun ml_enclose bg en source =
-  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\<close>
+  ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;\<close>
 
 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt)
 
@@ -48,7 +48,7 @@
 let
   val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt)
 in 
-   Pretty.str (Input.source_content code_txt)
+   Pretty.str (fst (Input.source_content code_txt))
 end
 
 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
@@ -129,7 +129,7 @@
 \<close>
 
 ML%linenosgray\<open>fun ml_pat pat code =
-  ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code\<close>
+  ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close>
 
 (*
 ML %grayML{*fun ml_pat code_txt pat =
@@ -154,8 +154,8 @@
 fun output_ml_resp ctxt (code_txt, pat) =
 let
   val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt)
-  val code = space_explode "\n" (Input.source_content code_txt)
-  val resp = add_resp (space_explode "\n" (Input.source_content pat))
+  val code = space_explode "\n" (fst (Input.source_content code_txt))
+  val resp = add_resp (space_explode "\n" (fst (Input.source_content pat)))
 in 
    Pretty.str (cat_lines (code @ resp))
 end