doc-src/IsarImplementation/Thy/prelim.thy
changeset 21862 13e9febe3080
parent 21852 7f2853bd54bf
child 22438 96e650157b1e
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Fri Dec 15 00:08:16 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri Dec 15 00:08:50 2006 +0100
@@ -702,8 +702,8 @@
   @{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} \\
@@ -731,8 +731,8 @@
   \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