# HG changeset patch
# User wenzelm
# Date 1237840811 -3600
# Node ID 2f64540707d6420fa8cf0580e6b1108d30103a3d
# Parent  9bb872667af6994ade070d326d646e83850288f6
de-camelized ML_Name_Space;

diff -r 9bb872667af6 -r 2f64540707d6 src/Pure/ML-Systems/ml_name_space.ML
--- 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,