src/Pure/General/name_space.ML

     (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
 
-structure NameSpace: NAME_SPACE =
+structure Name_Space: NAME_SPACE =
 struct
 
 
 (** name spaces **)
 

 
 
 (* datatype T *)
 
 datatype T =
-  NameSpace of
+  Name_Space of
     (string list * string list) Symtab.table *   (*internals, hidden internals*)
     entry Symtab.table;
 
-val empty = NameSpace (Symtab.empty, Symtab.empty);
-
-fun lookup (NameSpace (tab, _)) xname =
+val empty = Name_Space (Symtab.empty, Symtab.empty);
+
+fun lookup (Name_Space (tab, _)) xname =
   (case Symtab.lookup tab xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
   | SOME ([name], _) => (name, true)
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, entries)) name =
+fun get_accesses (Name_Space (_, entries)) name =
   (case Symtab.lookup entries name of
     NONE => [name]
   | SOME {externals, ...} => externals);
 
-fun valid_accesses (NameSpace (tab, _)) name =
+fun valid_accesses (Name_Space (tab, _)) name =
   Symtab.fold (fn (xname, (names, _)) =>
     if not (null names) andalso hd names = name then cons xname else I) tab [];
 
 
 (* intern and extern *)

 
 (* basic operations *)
 
 local
 
-fun map_space f xname (NameSpace (tab, entries)) =
-  NameSpace (Symtab.map_default (xname, ([], [])) f tab, entries);
+fun map_space f xname (Name_Space (tab, entries)) =
+  Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries);
 
 in
 
 val del_name = map_space o apfst o remove (op =);
 fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));

     end;
 
 
 (* merge *)
 
-fun merge (NameSpace (tab1, entries1), NameSpace (tab2, entries2)) =
+fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) =
   let
     val tab' = (tab1, tab2) |> Symtab.join
       (K (fn ((names1, names1'), (names2, names2')) =>
         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
         then raise Symtab.SAME

         if #id entry1 = #id entry2 then raise Symtab.SAME
         else
           error ("Duplicate declaration " ^
             quote (str_of_entry true (name, entry1)) ^ " vs. " ^
             quote (str_of_entry true (name, entry2))));
-  in NameSpace (tab', entries') end;
+  in Name_Space (tab', entries') end;
 
 
 
 (** naming contexts **)
 

 fun external_names naming = #2 o accesses naming o Binding.qualified_name;
 
 
 (* declaration *)
 
-fun new_entry strict entry (NameSpace (tab, entries)) =
+fun new_entry strict entry (Name_Space (tab, entries)) =
   let
     val entries' =
       (if strict then Symtab.update_new else Symtab.update) entry entries
         handle Symtab.DUP _ =>
           error ("Duplicate declaration " ^ quote (str_of_entry true entry));
-  in NameSpace (tab, entries') end;
+  in Name_Space (tab, entries') end;
 
 fun declare strict naming binding space =
   let
     val names = full naming binding;
     val name = Long_Name.implode names;

 fun dest_table tab = map (apfst #1) (ext_table tab);
 fun extern_table tab = map (apfst #2) (ext_table tab);
 
 end;
 
-structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
 open Basic_Name_Space;