equal
deleted
inserted
replaced
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 |