diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/Recipes/Antiquotes.thy
--- a/ProgTutorial/Recipes/Antiquotes.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -46,7 +46,7 @@
 let
   val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none}
 in
-  (ML_Context.eval_source_in (SOME ctxt) false srcpos; 
+  (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; 
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 end
 
@@ -83,7 +83,7 @@
 let
   val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}
 in
-  (ML_Context.eval_source_in (SOME ctxt) false srcpos;
+  (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 end
 
@@ -143,7 +143,7 @@
   (let
      val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}
    in
-     ML_Context.eval_source_in (SOME ctxt) false srcpos 
+     ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos 
    end;
    let 
      val code_output = space_explode "\n" code_txt