# HG changeset patch
# User wenzelm
# Date 1681593068 -7200
# Node ID cba7246c2c32bc571ded8d15302cc7e1d8f09596
# Parent  21bb32a7fd58297b6b12f40c3b81373021e5e112# Parent  e1636a54dab069792c90f960962c9317241db128
merged

diff -r 21bb32a7fd58 -r cba7246c2c32 src/Pure/General/long_name.ML
--- 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;
diff -r 21bb32a7fd58 -r cba7246c2c32 src/Pure/General/name_space.ML
--- 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'