# HG changeset patch
# User wenzelm
# Date 1427822204 -7200
# Node ID 547bf78e5d4d66d738885a909adee244cdab56fd
# Parent  30687c3f2b10d19268c16d4414c54990ce16056f
tuned;

diff -r 30687c3f2b10 -r 547bf78e5d4d src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 17:34:52 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 19:16:44 2015 +0200
@@ -110,7 +110,7 @@
 
 (* internal names *)
 
-type internals = (string list * string list) Change_Table.T;  (*xname -> visible, hidden*)
+type internals = (string list * string list) Change_Table.T;
 
 fun map_internals f xname : internals -> internals =
   Change_Table.map_default (xname, ([], [])) f;
@@ -119,14 +119,15 @@
 fun del_name_extra name =
   map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
 val add_name = map_internals o apfst o update (op =);
-val add_name' = map_internals o apsnd o update (op =);
+fun hide_name name = map_internals (apsnd (update (op =) name)) name;
 
 
 (* datatype T *)
 
 datatype T =
   Name_Space of
-   {kind: string, internals: internals,
+   {kind: string,
+    internals: internals,  (*xname -> visible, hidden*)
     entries: (xstring list * entry) Change_Table.T};  (*name -> externals, entry*)
 
 fun make_name_space (kind, internals, entries) =
@@ -377,7 +378,7 @@
       val _ = Change_Table.defined entries name orelse error (undefined kind name);
       val names = valid_accesses space name;
       val internals' = internals
-        |> add_name' name name
+        |> hide_name name
         |> fold (del_name name)
           (if fully then names else inter (op =) [Long_Name.base_name name] names)
         |> fold (del_name_extra name) (get_accesses space name);