updated;

--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Dec 15 00:08:16 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Dec 15 00:08:50 2006 +0100
@@ -137,7 +137,7 @@
         &            & \isa{{\isasymdown}} \\
         &            & \isa{FOL} \\
         & $\swarrow$ &              & $\searrow$ & \\
-  $Nat$ &            &              &            & \isa{List} \\
+  \isa{Nat} &    &              &            & \isa{List} \\
         & $\searrow$ &              & $\swarrow$ \\
         &            & \isa{Length} \\
         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
@@ -810,8 +810,8 @@
   \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
   \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| \\
+  \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
+  \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
   \end{mldecls}
   \begin{mldecls}
   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
@@ -839,7 +839,7 @@
   \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
   appends two qualified names.
 
-  \item \verb|NameSpace.pack|~\isa{name} and \verb|NameSpace.unpack|~\isa{names} convert between the packed string
+  \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
   representation and the explicit list form of qualified names.
 
   \item \verb|NameSpace.naming| represents the abstract concept of

--- 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