merged

--- a/src/Pure/General/long_name.ML	Sat Apr 15 23:02:01 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 23:11:08 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;

--- a/src/Pure/General/name_space.ML	Sat Apr 15 23:02:01 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 15 23:11:08 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'