equal
deleted
inserted
replaced
967 Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))]))) |
967 Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))]))) |
968 |> fold (curry Graph.add_edge value_name) deps; |
968 |> fold (curry Graph.add_edge value_name) deps; |
969 val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name]; |
969 val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name]; |
970 val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' |
970 val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' |
971 ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; |
971 ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; |
972 in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end; |
972 in ML_Context.evaluate ctxt false reff sml_code end; |
973 in eval'' thy (rpair eval') ct end; |
973 in eval'' thy (rpair eval') ct end; |
974 |
974 |
975 fun eval_term reff = eval Code_Thingol.eval_term I reff; |
975 fun eval_term reff = eval Code_Thingol.eval_term I reff; |
976 |
976 |
977 |
977 |