# HG changeset patch
# User wenzelm
# Date 1168456646 -3600
# Node ID d7c91b2f5a9e95991645e0e2ff6d5ebddf38e6f7
# Parent  858016d004491136aed29c4a508e066b88a6e285
removed NameSpace.split -- use qualifier/base instead;

diff -r 858016d00449 -r d7c91b2f5a9e src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Jan 10 20:16:52 2007 +0100
+++ b/src/Pure/General/name_space.ML	Wed Jan 10 20:17:26 2007 +0100
@@ -28,7 +28,6 @@
   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
@@ -88,9 +87,6 @@
 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
diff -r 858016d00449 -r d7c91b2f5a9e src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Wed Jan 10 20:16:52 2007 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Wed Jan 10 20:17:26 2007 +0100
@@ -336,9 +336,10 @@
 
 fun labelled_name thy name =
   let
-    val (base, nsp) = NameSpace.split name
+    val nam = NameSpace.qualifier name;
+    val nsp = NameSpace.base name;
   in case AList.lookup (op =) nsp_mapping nsp
-   of SOME msg => msg ^ " " ^ quote base
+   of SOME msg => msg ^ " " ^ quote nam
     | NONE => error ("illegal shallow name space: " ^ quote nsp)
   end;