doc-src/IsarImplementation/Thy/Integration.thy

   is achieved eventually.
 *}
 
 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"} \\
   @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
   @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]

   @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
   \end{mldecls}
 
   \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
   use_thys} should be used exclusively.
 

   import header of a theory, without performing the merge of the
   result.  By loading a whole sub-graph of theories like that, the
   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.
 
   \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
   descendants from the theory database.