--- a/src/Pure/ML-Systems/polyml.ML Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Mon Dec 11 19:05:23 2006 +0100
@@ -111,6 +111,8 @@
if verbose then print (output ()) else ()
end;
+fun use_file _ _ name = use name;
+
(*eval command line arguments*)
local