# HG changeset patch
# User wenzelm
# Date 1206635757 -3600
# Node ID feeb83f9657fb9b363d67a48ff01f6f081d931b4
# Parent  e38f7e1c07ce4ad2a5d31b5e2a9c4377aedf05bc
tuned comments;
tuned;

diff -r e38f7e1c07ce -r feeb83f9657f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Mar 27 17:35:56 2008 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 27 17:35:57 2008 +0100
@@ -6,8 +6,8 @@
 are considered global; no support for absolute addressing.
 *)
 
-type bstring = string;    (*names to be bound / internalized*)
-type xstring = string;    (*externalized names / to be printed*)
+type bstring = string;    (*names to be bound*)
+type xstring = string;    (*external names*)
 
 signature BASIC_NAME_SPACE =
 sig
@@ -157,14 +157,14 @@
   let
     fun valid unique xname =
       let val (name', uniq) = lookup space xname
-      in name = name' andalso (uniq orelse (not unique)) end;
+      in name = name' andalso (uniq orelse not unique) end;
 
-    fun ex [] = if valid false name then name else hidden name
-      | ex (nm :: nms) = if valid (! unique_names) nm then nm else ex nms;
+    fun ext [] = if valid false name then name else hidden name
+      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
   in
     if ! long_names then name
     else if ! short_names then base name
-    else ex (get_accesses space name)
+    else ext (get_accesses space name)
   end;
 
 
@@ -176,14 +176,11 @@
   NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
     (fn (entry, _) => (f entry, stamp ())) tab, xtab);
 
-fun del (name: string) = remove (op =) name;
-fun add name names = name :: del name names;
-
 in
 
-val del_name = map_space o apfst o del;
-val add_name = map_space o apfst o add;
-val add_name' = map_space o apsnd o add;
+val del_name = map_space o apfst o remove (op =);
+val add_name = map_space o apfst o update (op =);
+val add_name' = map_space o apsnd o update (op =);
 
 end;
 
@@ -222,6 +219,7 @@
   in NameSpace (tab', xtab') end;
 
 
+
 (** naming contexts **)
 
 (* datatype naming *)