diff -r e5b2dd8db7c8 -r 36cf92f63a44 src/Tools/code/code_target.ML
--- 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;