diff -r 762cb38a3147 -r 87f0f707a5f8 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Aug 16 21:55:11 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sun Aug 16 23:14:27 2015 +0200
@@ -4,9 +4,23 @@
 Compatibility wrapper for Poly/ML.
 *)
 
-val ml_initial_val =
-  List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-    (#allVal PolyML.globalNameSpace ());
+(* initial ML name space *)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val initial_val =
+    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+      (#allVal global ());
+  val initial_type = #allType global ();
+  val initial_fixity = #allFix global ();
+  val initial_structure = #allStruct global ();
+  val initial_signature = #allSig global ();
+  val initial_functor = #allFunct global ();
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+end;
 
 
 (* ML system operations *)
@@ -159,16 +173,7 @@
 
 structure ML_Name_Space =
 struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-  val initial_val = ml_initial_val;
-  val initial_type = #allType global ();
-  val initial_fixity = #allFix global ();
-  val initial_structure = #allStruct global ();
-  val initial_signature = #allSig global ();
-  val initial_functor = #allFunct global ();
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
+  open ML_Name_Space;
   val display_val = pretty_ml o PolyML.NameSpace.displayVal;
 end;