# HG changeset patch
# User wenzelm
# Date 1683461928 -7200
# Node ID 21cdcd120a78f71864d7ead6cd695db7ccbd015d
# Parent  f83702560730990e701aa10864f7fd8d8767d478
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';

diff -r f83702560730 -r 21cdcd120a78 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun May 07 12:30:11 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sun May 07 14:18:48 2023 +0200
@@ -232,22 +232,6 @@
 fun get_aliases space name =
   lookup_aliases space name @ [suppress_entry space name];
 
-fun is_valid_access space name xname =
-  (case lookup_internals space xname of
-    name' :: _ => name = name'
-  | _ => false);
-
-fun valid_accesses {intern, aliases} space name =
-  let
-    fun accesses (suppress, a) =
-      make_accesses {intern = intern} NONE suppress a
-      |> filter (is_valid_access space a);
-  in
-    if aliases then maps accesses (get_aliases space name)
-    else accesses (suppress_entry space name)
-  end;
-
-
 fun gen_markup def space name =
   (case lookup_entries space name of
     NONE => Markup.intensify
@@ -528,10 +512,11 @@
   space |> map_name_space (fn (kind, internals, internals_hidden, entries, aliases) =>
     let
       val _ = the_entry space name;
+      val hide_names = get_aliases space name;
       val accesses =
-        valid_accesses {intern = true, aliases = true} space name
+        maps (uncurry (make_accesses {intern = true} NONE)) hide_names
         |> not fully ? inter Long_Name.eq_chunks [Long_Name.base_chunks name];
-      val accesses' = valid_accesses {intern = false, aliases = false} space name;
+      val accesses' = maps (uncurry (make_accesses {intern = false} NONE)) hide_names;
       val internals' = internals
         |> fold (del_internals name) accesses
         |> fold (del_internals' name) accesses';