diff -r 34382a1f37d6 -r 33b7372e87ad src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Sun Aug 03 17:38:59 2014 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Fri Aug 01 13:59:34 2014 +0200 @@ -50,8 +50,10 @@ ## invoke code generation -FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \ - (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \ +FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \ + (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \ + ML_Compiler.flags \ + {delimited=true, text=ml_cmd, pos=Position.none})) \ handle _ => exit 1;" ACTUAL_CMD="val thyname = \"$THYNAME\"; \