| changeset 56618 | 874bdedb2313 |
| parent 56333 | 38f1422ef473 |
| child 58991 | 92b6f4e68c5a |
--- a/src/Pure/ML/ml_compiler_polyml.ML Thu Apr 17 14:52:23 2014 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Sat Apr 19 17:23:05 2014 +0200 @@ -70,7 +70,7 @@ fun eval (flags: flags) pos toks = let val _ = Secure.secure_mltext (); - val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space; + val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags} val opt_context = Context.thread_data ();