src/Pure/General/name_space.ML

   val explode: string -> string list
   val append: string -> string -> string
   val qualified: string -> string -> string
   val base: string -> string
   val qualifier: string -> string
+  val split: string -> string * string
   val map_base: (string -> string) -> string -> string
   val suffixes_prefixes: 'a list -> 'a list list
   val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
   val accesses: string -> string list
   val accesses': string -> string list

   | base name = List.last (explode_name name);
 
 fun qualifier "" = ""
   | qualifier name = implode_name (#1 (split_last (explode_name name)));
 
+fun split "" = ("", "")
+  | split name = (apfst implode_name o split_last o explode_name) name;
+
 fun map_base _ "" = ""
   | map_base f name =
       let val names = explode_name name
       in implode_name (nth_map (length names - 1) f names) end;