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"];