--- 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