diff -r 1c310b042d69 -r f809deffdd8f src/Pure/General/file.ML
--- 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;