--- a/src/Pure/General/file.ML Thu Jan 19 21:22:19 2006 +0100
+++ b/src/Pure/General/file.ML Thu Jan 19 21:22:20 2006 +0100
@@ -147,6 +147,6 @@
(* use ML files *)
-val use = Output.toplevel_errors (use o platform_path);
+val use = Output.ML_errors use o platform_path;
end;