src/Pure/ML/ml_compiler.ML

--- a/src/Pure/ML/ml_compiler.ML	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -144,7 +144,10 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
+    val space =
+      (case (#SML flags orelse #exchange flags, ML_Recursive.get ()) of
+        (false, SOME space) => space
+      | _ => ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags});
     val opt_context = Context.get_generic_context ();
 
 
@@ -264,7 +267,7 @@
 
     val _ =
       (while not (List.null (! input_buffer)) do
-        PolyML.compiler (get, parameters) ())
+        ML_Recursive.recursive space (fn () => PolyML.compiler (get, parameters) ()))
       handle exn =>
         if Exn.is_interrupt exn then Exn.reraise exn
         else