# HG changeset patch
# User wenzelm
# Date 1170778814 -3600
# Node ID ce77e962200249302deab080d95a7fa1b6ceaff5
# Parent  b4e26fba2a1a4d9d2eb6913f2fa250ae96d8cdaf
pervasive exception Option;
fixed use_file;

diff -r b4e26fba2a1a -r ce77e9622002 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Feb 06 17:06:44 2007 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Feb 06 17:20:14 2007 +0100
@@ -67,6 +67,9 @@
   structure FileSys = FileSys
 end;
 
+exception Option = Option.Option;
+
+
 (*limit the printing depth*)
 fun print_depth n =
  (Meta.printDepth := n div 2;
@@ -144,7 +147,7 @@
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ name = PolyML.use name;
+fun use_file _ _ name = use name;