src/Tools/Code/code_runtime.ML
changeset 55684 ee49b4f7edc8
parent 55683 5732a55b9232
child 55757 9fc71814b8c1
equal deleted inserted replaced
55683:5732a55b9232 55684:ee49b4f7edc8
    87   let
    87   let
    88     val ctxt = Proof_Context.init_global thy;
    88     val ctxt = Proof_Context.init_global thy;
    89   in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
    89   in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
    90 
    90 
    91 fun obtain_evaluator thy some_target program consts expr =
    91 fun obtain_evaluator thy some_target program consts expr =
    92   Code_Target.evaluator thy (the_default target some_target) program consts expr
    92   Code_Target.evaluator thy (the_default target some_target) program consts false expr
    93   |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    93   |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    94 
    94 
    95 fun obtain_evaluator' thy some_target program =
    95 fun obtain_evaluator' thy some_target program =
    96   obtain_evaluator thy some_target program o map Constant;
    96   obtain_evaluator thy some_target program o map Constant;
    97 
    97