src/Pure/General/name_space.ML
changeset 21914 77372f38aa98
parent 21858 05f57309170c
child 21962 279b129498b6
     1.1 --- a/src/Pure/General/name_space.ML	Wed Dec 27 19:10:04 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Dec 27 19:10:05 2006 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4    val qualified: string -> string -> string
     1.5    val base: string -> string
     1.6    val qualifier: string -> string
     1.7 +  val split: string -> string * string
     1.8    val map_base: (string -> string) -> string -> string
     1.9    val suffixes_prefixes: 'a list -> 'a list list
    1.10    val suffixes_prefixes_split: int -> int -> 'a list -> 'a list list
    1.11 @@ -87,6 +88,9 @@
    1.12  fun qualifier "" = ""
    1.13    | qualifier name = implode_name (#1 (split_last (explode_name name)));
    1.14  
    1.15 +fun split "" = ("", "")
    1.16 +  | split name = (apfst implode_name o split_last o explode_name) name;
    1.17 +
    1.18  fun map_base _ "" = ""
    1.19    | map_base f name =
    1.20        let val names = explode_name name