changeset 25204 | 36cf92f63a44 |
parent 25191 | e1146aa1e3e3 |
child 25538 | 58e8ba3b792b |
--- a/src/Tools/code/code_target.ML Fri Oct 26 17:55:33 2007 +0200 +++ b/src/Tools/code/code_target.ML Fri Oct 26 19:58:32 2007 +0200 @@ -1709,7 +1709,7 @@ val code' = CodeThingol.add_value_stmt (t, ty) code; val label = "evaluation in SML"; fun eval () = (seri (SOME [CodeName.value_name]) code'; - evaluate (ref_name, reff) label Output.ml_output (!eval_verbose) val_args); + ML_Context.evaluate Output.ml_output (!eval_verbose) (ref_name, reff) val_args); in NAMED_CRITICAL label eval end;