# HG changeset patch
# User wenzelm
# Date 1682972341 -7200
# Node ID 00c38dd0f30f131be15651ce6c289378bbc56629
# Parent  99df2576107f4f7594e5bcc5360dc6f566382f36
tuned;

diff -r 99df2576107f -r 00c38dd0f30f src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon May 01 13:09:53 2023 +0200
+++ b/src/Pure/General/name_space.ML	Mon May 01 22:19:01 2023 +0200
@@ -216,12 +216,11 @@
 
 fun intern_chunks space xname =
   (case the_default ([], []) (lookup_internals space xname) of
-    ([name], _) => (name, true)
-  | (name :: _, _) => (name, false)
-  | ([], []) => (Long_Name.hidden (Long_Name.implode_chunks xname), true)
-  | ([], name' :: _) => (Long_Name.hidden name', true));
+    (name :: rest, _) => {name = name, unique = null rest}
+  | ([], name' :: _) => {name = Long_Name.hidden name', unique = true}
+  | ([], []) => {name = Long_Name.hidden (Long_Name.implode_chunks xname), unique = true});
 
-fun intern space = #1 o intern_chunks space o Long_Name.make_chunks;
+fun intern space = #name o intern_chunks space o Long_Name.make_chunks;
 
 fun is_valid_access space name xname =
   (case lookup_internals space xname of
@@ -242,8 +241,8 @@
     val names_unique = Config.get ctxt names_unique;
 
     fun valid require_unique xname =
-      let val (name', is_unique) = intern_chunks space xname
-      in name = name' andalso (not require_unique orelse is_unique) end;
+      let val {name = name', unique} = intern_chunks space xname
+      in name = name' andalso (not require_unique orelse unique) end;
 
     fun extern [] =
           if valid false (Long_Name.make_chunks name) then name