--- a/src/Pure/General/name_space.ML Wed Dec 27 19:10:04 2006 +0100
+++ b/src/Pure/General/name_space.ML Wed Dec 27 19:10:05 2006 +0100
@@ -28,6 +28,7 @@
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
@@ -87,6 +88,9 @@
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