# HG changeset patch
# User wenzelm
# Date 1158176485 -7200
# Node ID 448594cbd82b24ef9790608492b3c0a955cee115
# Parent  1ca27b3ed2e72036c95398a5bb6730f9449b6b07
renamed NameSpace.drop_base to NameSpace.qualifier;

diff -r 1ca27b3ed2e7 -r 448594cbd82b doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Sep 13 12:40:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Sep 13 21:41:25 2006 +0200
@@ -802,7 +802,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
-  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\  %FIXME qualifier
+  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
   \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
   \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
   \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
@@ -823,7 +823,7 @@
   \item \verb|NameSpace.base|~\isa{name} returns the base name of a
   qualified name.
 
-  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
+  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
   of a qualified name.
 
   \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
diff -r 1ca27b3ed2e7 -r 448594cbd82b doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Sep 13 12:40:39 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Sep 13 21:41:25 2006 +0200
@@ -694,7 +694,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML NameSpace.base: "string -> string"} \\
-  @{index_ML NameSpace.drop_base: "string -> string"} \\  %FIXME qualifier
+  @{index_ML NameSpace.qualifier: "string -> string"} \\
   @{index_ML NameSpace.append: "string -> string -> string"} \\
   @{index_ML NameSpace.pack: "string list -> string"} \\
   @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
@@ -715,7 +715,7 @@
   \item @{ML NameSpace.base}~@{text "name"} returns the base name of a
   qualified name.
 
-  \item @{ML NameSpace.drop_base}~@{text "name"} returns the qualifier
+  \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
   of a qualified name.
 
   \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
diff -r 1ca27b3ed2e7 -r 448594cbd82b src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Sep 13 12:40:39 2006 +0200
+++ b/src/Pure/General/name_space.ML	Wed Sep 13 21:41:25 2006 +0200
@@ -27,7 +27,7 @@
   val append: string -> string -> string
   val qualified: string -> string -> string
   val base: string -> string
-  val drop_base: string -> string
+  val qualifier: 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
@@ -84,8 +84,8 @@
 fun base "" = ""
   | base name = List.last (unpack name);
 
-fun drop_base "" = ""
-  | drop_base name = pack (#1 (split_last (unpack name)));
+fun qualifier "" = ""
+  | qualifier name = pack (#1 (split_last (unpack name)));
 
 fun map_base _ "" = ""
   | map_base f name =
@@ -248,7 +248,7 @@
 fun add_path elems (Naming (path, policy)) =
   if elems = "//" then Naming ("", (qualified, #2 policy))
   else if elems = "/" then Naming ("", policy)
-  else if elems = ".." then Naming (drop_base path, policy)
+  else if elems = ".." then Naming (qualifier path, policy)
   else Naming (append path elems, policy);
 
 fun no_base_names (Naming (path, (qualify, accs))) =