src/Pure/ML/ml_name_space.ML
changeset 62902 3c0f53eae166
parent 62890 728aa05e9433
child 62910 f37878ebba65
--- a/src/Pure/ML/ml_name_space.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -61,7 +61,7 @@
   (* bootstrap environment *)
 
   val bootstrap_values =
-    ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+    ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
   val bootstrap_structures =
     ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data"];