doc-src/IsarImplementation/Thy/document/integration.tex

 %
 \isatagmlref
 %
 \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
   evaluation of a function body is delayed until actual runtime.