doc-src/IsarImplementation/Thy/document/prelim.tex

 \isatagmlref
 %
 \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]
   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\

   \begin{description}
 
   \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}}}
   appends two qualified names.