src/Pure/General/name_space.ML

   val is_qualified: string -> bool
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
   val qualified: string -> string -> string
-  val base: string -> string
+  val base_name: string -> string
   val qualifier: string -> string
-  val map_base: (string -> string) -> string -> string
+  val map_base_name: (string -> string) -> string -> string
   type T
   val empty: T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->

 
 fun qualified path name =
   if path = "" orelse name = "" then name
   else path ^ separator ^ name;
 
-fun base "" = ""
-  | base name = List.last (explode_name name);
+fun base_name "" = ""
+  | base_name name = List.last (explode_name name);
 
 fun qualifier "" = ""
   | qualifier name = implode_name (#1 (split_last (explode_name name)));
 
-fun map_base _ "" = ""
-  | map_base f name =
+fun map_base_name _ "" = ""
+  | map_base_name f name =
       let val names = explode_name name
       in implode_name (nth_map (length names - 1) f names) end;
 
 
 (* standard accesses *)

 
     fun ext [] = if valid false name then name else hidden name
       | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   in
     if long_names then name
-    else if short_names then base name
+    else if short_names then base_name name
     else ext (get_accesses space name)
   end;
 
 val long_names = ref false;
 val short_names = ref false;

     error ("Attempt to hide hidden name " ^ quote name)
   else
     let val names = valid_accesses space name in
       space
       |> add_name' name name
-      |> fold (del_name name) (if fully then names else names inter_string [base name])
+      |> fold (del_name name) (if fully then names else names inter_string [base_name name])
       |> fold (del_name_extra name) (get_accesses space name)
     end;
 
 
 (* merge *)