# HG changeset patch
# User wenzelm
# Date 1003431766 -7200
# Node ID f252646080fc71d0b9443516762f64999812da94
# Parent  ef3e51b1b4ec28572b5530a84c23040c72f72092
added map_base;

diff -r ef3e51b1b4ec -r f252646080fc src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Oct 18 21:02:26 2001 +0200
+++ b/src/Pure/General/name_space.ML	Thu Oct 18 21:02:46 2001 +0200
@@ -18,6 +18,7 @@
   val unpack: string -> string list
   val pack: string list -> string
   val base: string -> string
+  val map_base: (string -> string) -> string -> string
   val is_qualified: string -> bool
   val accesses: string -> string list
   type T
@@ -58,6 +59,11 @@
 val pack = space_implode separator;
 
 val base = last_elem o unpack;
+
+fun map_base f name =
+  let val uname = unpack name
+  in pack (map_nth_elem (length uname - 1) f uname) end;
+
 fun is_qualified name = length (unpack name) > 1;
 
 fun accesses name =