doc-src/IsarImplementation/Thy/prelim.thy

 text %mlref {*
   \begin{mldecls}
   @{index_ML NameSpace.base: "string -> string"} \\
   @{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"} \\
+  @{index_ML NameSpace.implode: "string list -> string"} \\
+  @{index_ML NameSpace.explode: "string -> string list"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type NameSpace.naming} \\
   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\

   of a qualified name.
 
   \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
   appends two qualified names.
 
-  \item @{ML NameSpace.pack}~@{text "name"} and @{ML
-  NameSpace.unpack}~@{text "names"} convert between the packed string
+  \item @{ML NameSpace.implode}~@{text "name"} and @{ML
+  NameSpace.explode}~@{text "names"} convert between the packed string
   representation and the explicit list form of qualified names.
 
   \item @{ML_type NameSpace.naming} represents the abstract concept of
   a naming policy.