diff -r b82f344f7922 -r ea6f846d8c4b src/Pure/ML-Systems/polyml.ML
--- 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