src/Tools/code/code_target.ML

       (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
     val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
     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;
 
 
 
 (** optional pretty serialization **)