1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Mar 08 17:26:14 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Mar 08 17:37:18 2009 +0100
     1.3 @@ -682,11 +682,11 @@
     1.4  
     1.5  text %mlref {*
     1.6    \begin{mldecls}
     1.7 -  @{index_ML NameSpace.base_name: "string -> string"} \\
     1.8 -  @{index_ML NameSpace.qualifier: "string -> string"} \\
     1.9 -  @{index_ML NameSpace.append: "string -> string -> string"} \\
    1.10 -  @{index_ML NameSpace.implode: "string list -> string"} \\
    1.11 -  @{index_ML NameSpace.explode: "string -> string list"} \\
    1.12 +  @{index_ML Long_Name.base_name: "string -> string"} \\
    1.13 +  @{index_ML Long_Name.qualifier: "string -> string"} \\
    1.14 +  @{index_ML Long_Name.append: "string -> string -> string"} \\
    1.15 +  @{index_ML Long_Name.implode: "string list -> string"} \\
    1.16 +  @{index_ML Long_Name.explode: "string -> string list"} \\
    1.17    \end{mldecls}
    1.18    \begin{mldecls}
    1.19    @{index_ML_type NameSpace.naming} \\
    1.20 @@ -706,17 +706,17 @@
    1.21  
    1.22    \begin{description}
    1.23  
    1.24 -  \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a
    1.25 +  \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a
    1.26    qualified name.
    1.27  
    1.28 -  \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
    1.29 +  \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
    1.30    of a qualified name.
    1.31  
    1.32 -  \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
    1.33 +  \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"}
    1.34    appends two qualified names.
    1.35  
    1.36 -  \item @{ML NameSpace.implode}~@{text "name"} and @{ML
    1.37 -  NameSpace.explode}~@{text "names"} convert between the packed string
    1.38 +  \item @{ML Long_Name.implode}~@{text "names"} and @{ML
    1.39 +  Long_Name.explode}~@{text "name"} convert between the packed string
    1.40    representation and the explicit list form of qualified names.
    1.41  
    1.42    \item @{ML_type NameSpace.naming} represents the abstract concept of

     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:26:14 2009 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:37:18 2009 +0100
     2.3 @@ -791,11 +791,11 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \begin{mldecls}
     2.7 -  \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\
     2.8 -  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
     2.9 -  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
    2.10 -  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
    2.11 -  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
    2.12 +  \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
    2.13 +  \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
    2.14 +  \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
    2.15 +  \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
    2.16 +  \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
    2.17    \end{mldecls}
    2.18    \begin{mldecls}
    2.19    \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
    2.20 @@ -815,16 +815,16 @@
    2.21  
    2.22    \begin{description}
    2.23  
    2.24 -  \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a
    2.25 +  \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
    2.26    qualified name.
    2.27  
    2.28 -  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
    2.29 +  \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
    2.30    of a qualified name.
    2.31  
    2.32 -  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
    2.33 +  \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
    2.34    appends two qualified names.
    2.35  
    2.36 -  \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
    2.37 +  \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
    2.38    representation and the explicit list form of qualified names.
    2.39  
    2.40    \item \verb|NameSpace.naming| represents the abstract concept of

     3.1 --- a/doc-src/antiquote_setup.ML	Sun Mar 08 17:26:14 2009 +0100
     3.2 +++ b/doc-src/antiquote_setup.ML	Sun Mar 08 17:37:18 2009 +0100
     3.3 @@ -153,7 +153,7 @@
     3.4  
     3.5  fun output_entity check markup index kind ctxt (logic, name) =
     3.6    let
     3.7 -    val hyper_name = "{" ^ NameSpace.append kind (NameSpace.append logic (clean_name name)) ^ "}";
     3.8 +    val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
     3.9      val hyper =
    3.10        enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
    3.11        index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";