--- a/src/Pure/General/file.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/General/file.ML Sat Jan 14 17:14:06 2006 +0100
@@ -147,6 +147,6 @@
(* use ML files *)
-val use = use o platform_path;
+val use = Output.toplevel_errors (use o platform_path);
end;