# HG changeset patch
# User wenzelm
# Date 1236086165 -3600
# Node ID 3951aab916fdc96283fc01606dea09cbe289c8d4
# Parent  4b35b0f85b42235f878bbd239928319af7963e3c
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

diff -r 4b35b0f85b42 -r 3951aab916fd src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 03 14:08:53 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 03 14:16:05 2009 +0100
@@ -133,19 +133,10 @@
   | SOME ((name :: _, _), _) => (name, false)
   | SOME (([], name' :: _), _) => (hidden name', true));
 
-fun ex_mapsto_in (NameSpace (tab, _)) name xname =
-    (case Symtab.lookup tab xname of
-      SOME ((name'::_, _), _) => name' = name
-    | _ => false);
-
-fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
+fun get_accesses (NameSpace (_, tab)) name =
   (case Symtab.lookup tab name of
     NONE => [name]
-  | SOME (xnames, _) => if valid_only
-                        then filter (ex_mapsto_in ns name) xnames
-                        else xnames);
-
-val get_accesses = get_accesses' true;
+  | SOME (xnames, _) => xnames);
 
 fun put_accesses name xnames (NameSpace (tab, xtab)) =
   NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
@@ -169,7 +160,7 @@
   in
     if ! long_names then name
     else if ! short_names then base name
-    else ext (get_accesses' false space name)
+    else ext (get_accesses space name)
   end;
 
 
@@ -203,7 +194,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' false space name)
+      |> fold (del_name_extra name) (get_accesses space name)
     end;