# HG changeset patch
# User wenzelm
# Date 1213383883 -7200
# Node ID ef2f01da7a127546434306f552bea8dab0ce13db
# Parent  bbf4cbc69243a2bde7b294134b7ce870a9984836
hide: delete all accesses from extra names -- reduces ambiguity in extern;

diff -r bbf4cbc69243 -r ef2f01da7a12 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Jun 13 21:04:42 2008 +0200
+++ b/src/Pure/General/name_space.ML	Fri Jun 13 21:04:43 2008 +0200
@@ -179,6 +179,7 @@
 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));
 val add_name = map_space o apfst o update (op =);
 val add_name' = map_space o apsnd o update (op =);
 
@@ -197,6 +198,7 @@
       space
       |> add_name' name name
       |> fold (del_name name) (if fully then names else names inter_string [base name])
+      |> fold (del_name_extra name) (get_accesses space name)
     end;