# HG changeset patch
# User haftmann
# Date 1167243005 -3600
# Node ID 77372f38aa98d322401e610c395eed302c958b1b
# Parent  1224048fb8f9e5f1d6c492c57ae93c2b8e96cf02
added split

diff -r 1224048fb8f9 -r 77372f38aa98 src/Pure/General/name_space.ML
--- 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