--- 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