src/Pure/General/name_space.ML
changeset 22057 d7c91b2f5a9e
parent 21962 279b129498b6
child 23086 12320f6e2523
     1.1 --- a/src/Pure/General/name_space.ML	Wed Jan 10 20:16:52 2007 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Jan 10 20:17:26 2007 +0100
     1.3 @@ -28,7 +28,6 @@
     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 @@ -88,9 +87,6 @@
    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