diff -r 07875394618e -r fed088a475f9 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 22:08:02 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 22:08:03 2007 +0100
@@ -302,7 +302,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{the-context}\verb|the_context: unit -> theory| \\
-  \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
+  \indexml{ML-Context.$>$$>$ }\verb|ML_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|Context.>>|~\isa{f} applies theory transformation
+  \item \verb|ML_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