diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 13:18:10 2014 +0100
@@ -74,10 +74,12 @@
 
 (* eval ML source tokens *)
 
-fun eval verbose pos toks =
+type flags = {SML: bool, verbose: bool};
+
+fun eval {SML, verbose} pos toks =
   let
     val _ = Secure.secure_mltext ();
-    val space = ML_Env.name_space;
+    val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
     val opt_context = Context.thread_data ();