| changeset 62495 | 83db706d7771 |
| parent 62493 | dd154240a53c |
| child 62501 | 98fa1f9a292f |
--- a/src/Pure/ML/ml_compiler.ML Tue Mar 01 22:11:36 2016 +0100 +++ b/src/Pure/ML/ml_compiler.ML Tue Mar 01 22:49:33 2016 +0100 @@ -149,7 +149,7 @@ fun eval (flags: flags) pos toks = let val _ = Secure.deny_ml (); - val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}; + val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags}; val opt_context = Context.thread_data ();