# HG changeset patch
# User wenzelm
# Date 1279660581 -7200
# Node ID 814b1bca7f35501efc0da3b925bb89ba518db12f
# Parent  7f113caabcf441594b54642ee25283b9f697b8be
qualified Thy_Info.get_theory;

diff -r 7f113caabcf4 -r 814b1bca7f35 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Tue Jul 20 23:09:49 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Tue Jul 20 23:16:21 2010 +0200
@@ -360,9 +360,9 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML theory: "string -> theory"} \\
   @{index_ML use_thy: "string -> unit"} \\
   @{index_ML use_thys: "string list -> unit"} \\
+  @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
   @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
@@ -374,10 +374,6 @@
 
   \begin{description}
 
-  \item @{ML theory}~@{text A} retrieves the theory value presently
-  associated with name @{text A}.  Note that the result might be
-  outdated.
-
   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
   up-to-date wrt.\ the external file store, reloading outdated
   ancestors as required.  In batch mode, the simultaneous @{ML
@@ -390,6 +386,10 @@
   intrinsic parallelism can be exploited by the system, to speedup
   loading.
 
+  \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
+  presently associated with name @{text A}.  Note that the result
+  might be outdated.
+
   \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
   on theory @{text A} and all descendants.
 
diff -r 7f113caabcf4 -r 814b1bca7f35 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Tue Jul 20 23:09:49 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Tue Jul 20 23:16:21 2010 +0200
@@ -433,9 +433,9 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
   \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
   \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
+  \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
   \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
   \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
   \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
@@ -447,10 +447,6 @@
 
   \begin{description}
 
-  \item \verb|theory|~\isa{A} retrieves the theory value presently
-  associated with name \isa{A}.  Note that the result might be
-  outdated.
-
   \item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
   up-to-date wrt.\ the external file store, reloading outdated
   ancestors as required.  In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
@@ -462,6 +458,10 @@
   intrinsic parallelism can be exploited by the system, to speedup
   loading.
 
+  \item \verb|Thy_Info.get_theory|~\isa{A} retrieves the theory value
+  presently associated with name \isa{A}.  Note that the result
+  might be outdated.
+
   \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
   on theory \isa{A} and all descendants.