--- a/src/Pure/ML-Systems/ml_name_space.ML Mon Mar 23 17:21:42 2009 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML Mon Mar 23 21:40:11 2009 +0100
@@ -4,7 +4,7 @@
ML name space -- dummy version of Poly/ML 5.2 facility.
*)
-structure ML_NameSpace =
+structure ML_Name_Space =
struct
type valueVal = unit;
@@ -14,7 +14,7 @@
type signatureVal = unit;
type functorVal = unit;
-type nameSpace =
+type T =
{lookupVal: string -> valueVal option,
lookupType: string -> typeVal option,
lookupFix: string -> fixityVal option,
@@ -34,7 +34,7 @@
allSig: unit -> (string * signatureVal) list,
allFunct: unit -> (string * functorVal) list};
-val global: nameSpace =
+val global: T =
{lookupVal = fn _ => NONE,
lookupType = fn _ => NONE,
lookupFix = fn _ => NONE,