--- 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;
--- 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";