# HG changeset patch
# User wenzelm
# Date 1681590382 -7200
# Node ID e1636a54dab069792c90f960962c9317241db128
# Parent  30389d96d0d68894c974e00b5bad79ab0e583f49
tuned;

diff -r 30389d96d0d6 -r e1636a54dab0 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Sat Apr 15 15:19:58 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 22:26:22 2023 +0200
@@ -25,6 +25,7 @@
   val count_chunks: chunks -> int
   val size_chunks: chunks -> int
   val empty_chunks: chunks
+  val base_chunks: string -> chunks
   val make_chunks: int -> bool list -> string -> chunks
   val chunks: string -> chunks
   val explode_chunks: chunks -> string list
@@ -157,6 +158,9 @@
 
 val chunks = make_chunks 0 [];
 
+fun base_chunks name =
+  make_chunks (Int.max (0, count name - 1)) [] name;
+
 fun expand_chunks f (Chunks {count, size, mask, string}) =
   let
     val {string_end, chunk_end, ...} = string_ops string;
diff -r 30389d96d0d6 -r e1636a54dab0 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Apr 15 15:19:58 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 15 22:26:22 2023 +0200
@@ -490,9 +490,7 @@
       val xnames = filter (is_valid_access space name) accesses;
       val xnames' =
         if fully then xnames
-        else
-          let val base_name = Long_Name.chunks (Long_Name.base_name name)
-          in inter Long_Name.eq_chunks [base_name] xnames end;
+        else inter Long_Name.eq_chunks [Long_Name.base_chunks name] xnames;
       val internals' = internals
         |> hide_name name
         |> fold (del_name name) xnames'