# HG changeset patch
# User wenzelm
# Date 1236530238 -3600
# Node ID 790129514c2d1e3d8297ca8a0898eb8aaf800089
# Parent  577edc39b501ead0a97f6d017dc5b34f7adcbd29
adapted to structure Long_Name;

diff -r 577edc39b501 -r 790129514c2d doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Mar 08 17:37:18 2009 +0100
@@ -682,11 +682,11 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML NameSpace.base_name: "string -> string"} \\
-  @{index_ML NameSpace.qualifier: "string -> string"} \\
-  @{index_ML NameSpace.append: "string -> string -> string"} \\
-  @{index_ML NameSpace.implode: "string list -> string"} \\
-  @{index_ML NameSpace.explode: "string -> string list"} \\
+  @{index_ML Long_Name.base_name: "string -> string"} \\
+  @{index_ML Long_Name.qualifier: "string -> string"} \\
+  @{index_ML Long_Name.append: "string -> string -> string"} \\
+  @{index_ML Long_Name.implode: "string list -> string"} \\
+  @{index_ML Long_Name.explode: "string -> string list"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type NameSpace.naming} \\
@@ -706,17 +706,17 @@
 
   \begin{description}
 
-  \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a
+  \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a
   qualified name.
 
-  \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
+  \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
   of a qualified name.
 
-  \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
+  \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"}
   appends two qualified names.
 
-  \item @{ML NameSpace.implode}~@{text "name"} and @{ML
-  NameSpace.explode}~@{text "names"} convert between the packed string
+  \item @{ML Long_Name.implode}~@{text "names"} and @{ML
+  Long_Name.explode}~@{text "name"} convert between the packed string
   representation and the explicit list form of qualified names.
 
   \item @{ML_type NameSpace.naming} represents the abstract concept of
diff -r 577edc39b501 -r 790129514c2d doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Mar 08 17:37:18 2009 +0100
@@ -791,11 +791,11 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\
-  \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
-  \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
-  \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
-  \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
+  \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
+  \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
+  \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
+  \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
+  \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
@@ -815,16 +815,16 @@
 
   \begin{description}
 
-  \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a
+  \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
   qualified name.
 
-  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
+  \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
   of a qualified name.
 
-  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
+  \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
   appends two qualified names.
 
-  \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
+  \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
   representation and the explicit list form of qualified names.
 
   \item \verb|NameSpace.naming| represents the abstract concept of
diff -r 577edc39b501 -r 790129514c2d doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Sun Mar 08 17:37:18 2009 +0100
@@ -153,7 +153,7 @@
 
 fun output_entity check markup index kind ctxt (logic, name) =
   let
-    val hyper_name = "{" ^ NameSpace.append kind (NameSpace.append logic (clean_name name)) ^ "}";
+    val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
     val hyper =
       enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
       index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";