# HG changeset patch
# User wenzelm
# Date 1215532097 -7200
# Node ID 77ec4ad35ca2dd2fa92a462798b6221caa388349
# Parent  c8178a6a6480602d91ba1e64daf88f4fa1c0761f
more qualified ThyInfo names;

diff -r c8178a6a6480 -r 77ec4ad35ca2 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jul 08 16:19:24 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jul 08 17:48:17 2008 +0200
@@ -438,8 +438,8 @@
   \indexml{theory}\verb|theory: string -> theory| \\
   \indexml{use\_thy}\verb|use_thy: string -> unit| \\
   \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
-  \indexml{touch\_thy}\verb|touch_thy: string -> unit| \\
-  \indexml{remove\_thy}\verb|remove_thy: string -> unit| \\[1ex]
+  \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
+  \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
   \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> theory| \\
   \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
@@ -462,10 +462,10 @@
   import header of a theory, without performing the merge of the
   result, though.
 
-  \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
+  \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
   on theory \isa{A} and all descendants.
 
-  \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
+  \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
   descendants from the theory database.
 
   \item \verb|ThyInfo.begin_theory| is the basic operation behind a
diff -r c8178a6a6480 -r 77ec4ad35ca2 doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Tue Jul 08 16:19:24 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Tue Jul 08 17:48:17 2008 +0200
@@ -368,8 +368,8 @@
   @{index_ML theory: "string -> theory"} \\
   @{index_ML use_thy: "string -> unit"} \\
   @{index_ML use_thys: "string list -> unit"} \\
-  @{index_ML touch_thy: "string -> unit"} \\
-  @{index_ML remove_thy: "string -> unit"} \\[1ex]
+  @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
+  @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
   @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
   @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
   @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
@@ -392,10 +392,10 @@
   import header of a theory, without performing the merge of the
   result, though.
 
-  \item @{ML touch_thy}~@{text A} performs and @{text outdate} action
+  \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
   on theory @{text A} and all descendants.
 
-  \item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
+  \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
   descendants from the theory database.
 
   \item @{ML ThyInfo.begin_theory} is the basic operation behind a