src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 13:18:10 2014 +0100
@@ -4,6 +4,24 @@
 Compatibility wrapper for Poly/ML.
 *)
 
+(* 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 ();
+end;
+
+
 (* ML system operations *)
 
 use "ML-Systems/ml_system.ML";
@@ -94,13 +112,6 @@
 
 (* ML compiler *)
 
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
 use "ML-Systems/use_context.ML";
 use "ML-Systems/compiler_polyml.ML";