# HG changeset patch
# User wenzelm
# Date 1206567598 -3600
# Node ID 40932ee97ff83716330c0ce2311cbe738ba32381
# Parent  1ceabad5a2c8f79fb5ad8e8fe5da0b71459bb9a9
updated generated file;

diff -r 1ceabad5a2c8 -r 40932ee97ff8 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Wed Mar 26 22:39:57 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Wed Mar 26 22:39:58 2008 +0100
@@ -302,7 +302,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{the-context}\verb|the_context: unit -> theory| \\
-  \indexml{ML-Context.$>$$>$ }\verb|ML_Context.>> : (theory -> theory) -> unit| \\
+  \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
   \end{mldecls}
 
   \begin{description}
@@ -315,7 +315,7 @@
   should be avoided: code should either project out the desired
   information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
 
-  \item \verb|ML_Context.>>|~\isa{f} applies theory transformation
+  \item \verb|Context.>>|~\isa{f} applies theory transformation
   \isa{f} to the current theory of the {\ML} toplevel.  In order to
   work as expected, the theory should be still under construction, and
   the Isar language element that invoked the {\ML} compiler in the