# HG changeset patch
# User wenzelm
# Date 1683214194 -7200
# Node ID 93d2b378695929f73503c266ea9e0e37e544093f
# Parent  1d82061fbb1245ab3b1cfca75cdbb93f6c88c19e
tuned;

diff -r 1d82061fbb12 -r 93d2b3786959 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu May 04 11:42:04 2023 +0200
+++ b/src/Pure/General/name_space.ML	Thu May 04 17:29:54 2023 +0200
@@ -209,12 +209,13 @@
 fun kind_of (Name_Space {kind, ...}) = kind;
 fun lookup_internals (Name_Space {internals, ...}) = Long_Name.Chunks.lookup internals;
 fun lookup_entries (Name_Space {entries, ...}) = Change_Table.lookup entries;
-fun lookup_aliases (Name_Space {aliases, ...}) = Symtab.lookup aliases;
+fun lookup_aliases (Name_Space {aliases, ...}) = Symtab.lookup_list aliases;
+
+fun is_alias space c a =
+  c = a orelse member (op =) (lookup_aliases space c) a;
 
 fun get_aliases space name =
-  (case lookup_aliases space name of
-    NONE => [name]
-  | SOME aliases => aliases @ [name]);
+  lookup_aliases space name @ [name];
 
 fun is_valid_access space name xname =
   (case lookup_internals space xname of
@@ -292,8 +293,8 @@
     val names_unique = Config.get ctxt names_unique;
 
     fun extern_chunks require_unique a chunks =
-      let val {full_name = b, unique, ...} = intern_chunks space chunks in
-        if (not require_unique orelse unique) andalso member (op =) (get_aliases space b) a
+      let val {full_name = c, unique, ...} = intern_chunks space chunks in
+        if (not require_unique orelse unique) andalso is_alias space c a
         then SOME (Long_Name.implode_chunks chunks)
         else NONE
       end;