minor performance tuning: more elementary operations;

--- a/src/Pure/General/long_name.ML	Sat Apr 15 14:42:58 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 14:44:45 2023 +0200
@@ -12,6 +12,7 @@
   val is_qualified: string -> bool
   val qualifier: string -> string
   val base_name: string -> string
+  val map_base_name: (string -> string) -> string -> string
   val count: string -> int
   val hidden: string -> string
   val is_hidden: string -> bool
@@ -20,7 +21,6 @@
   val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
-  val map_base_name: (string -> string) -> string -> string
   type chunks
   val count_chunks: chunks -> int
   val size_chunks: chunks -> int
@@ -66,6 +66,10 @@
     val j = i + 1;
   in if i < 0 then name else String.substring (name, j, size name - j) end;
 
+fun map_base_name f name =
+  if name = "" then ""
+  else qualify (qualifier name) (f (base_name name));
+
 fun count "" = 0
   | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
 
@@ -80,11 +84,6 @@
 val implode = space_implode separator;
 val explode = space_explode separator;
 
-fun map_base_name _ "" = ""
-  | map_base_name f name =
-      let val names = explode name
-      in implode (nth_map (length names - 1) f names) end;
-
 
 (* compact representation of chunks *)