# HG changeset patch
# User wenzelm
# Date 1459794497 -7200
# Node ID 8e54fd480809dd17443efeb9c528045cde2e33d9
# Parent  dd5f3a6fee73d7a1a56e5762f7e48848b5dc4e9f
tuned;

diff -r dd5f3a6fee73 -r 8e54fd480809 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Mon Apr 04 20:20:47 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Mon Apr 04 20:28:17 2016 +0200
@@ -1,13 +1,11 @@
 (*  Title:      Pure/ML/ml_name_space.ML
     Author:     Makarius
 
-Name space for Poly/ML.
+ML name space, with initial entries for strict Standard ML.
 *)
 
 structure ML_Name_Space =
 struct
-  val critical_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
-
   open PolyML.NameSpace;
 
   type T = PolyML.NameSpace.nameSpace;
@@ -67,10 +65,9 @@
   val sml_fixity = #allFix global ();
   val sml_structure =
     List.filter (fn (a, _) =>
-      not (List.exists (fn b => a = b)
-        ["ML_System", "PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]))
+      List.all (fn b => a <> b)
+        ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"])
       (#allStruct global ());
-  val sml_signature =
-    List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
+  val sml_signature = #allSig global ();
   val sml_functor = #allFunct global ();
 end;
diff -r dd5f3a6fee73 -r 8e54fd480809 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 04 20:20:47 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 20:28:17 2016 +0200
@@ -4,9 +4,9 @@
 
 (* initial ML name space *)
 
-use "ML/ml_system.ML";
 use "ML/ml_name_space.ML";
 use "ML/ml_pervasive_initial.ML";
+use "ML/ml_system.ML";
 
 if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
 else use "ML/fixed_int_dummy.ML";