tuned, so codegen runs with current isabelle again
authorLars Noschinski <noschinl@in.tum.de>
Fri, 01 Aug 2014 13:59:34 +0200
changeset 5906733b7372e87ad
parent 59066 34382a1f37d6
child 59068 0ecc524797dc
tuned, so codegen runs with current isabelle again
src/Tools/Code/lib/Tools/codegen
     1.1 --- a/src/Tools/Code/lib/Tools/codegen	Sun Aug 03 17:38:59 2014 +0200
     1.2 +++ b/src/Tools/Code/lib/Tools/codegen	Fri Aug 01 13:59:34 2014 +0200
     1.3 @@ -50,8 +50,10 @@
     1.4  
     1.5  ## invoke code generation
     1.6  
     1.7 -FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
     1.8 -  (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
     1.9 +FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
    1.10 +    (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
    1.11 +    ML_Compiler.flags \
    1.12 +    {delimited=true, text=ml_cmd, pos=Position.none})) \
    1.13    handle _ => exit 1;"
    1.14  
    1.15  ACTUAL_CMD="val thyname = \"$THYNAME\"; \