--- a/doc-src/IsarImplementation/Thy/document/integration.tex Fri Jan 19 13:09:37 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Fri Jan 19 13:16:37 2007 +0100
@@ -301,18 +301,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{context}\verb|context: theory -> unit| \\
\indexml{the-context}\verb|the_context: unit -> theory| \\
\indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
\end{mldecls}
\begin{description}
- \item \verb|context|~\isa{thy} sets the {\ML} theory context to
- \isa{thy}. This is usually performed automatically by the system,
- when dropping out of the interactive Isar toplevel into {\ML}, or
- when Isar invokes {\ML} to process code from a string or a file.
-
\item \verb|the_context ()| refers to the theory context of the
{\ML} toplevel --- at compile time! {\ML} code needs to take care
to refer to \verb|the_context ()| correctly. Recall that