--- a/doc-src/IsarImplementation/Thy/document/integration.tex Fri Mar 28 20:02:04 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Fri Mar 28 20:08:11 2008 +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{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
\end{mldecls}
\begin{description}
@@ -315,13 +315,8 @@
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
- \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
- first place should be ready to accept the changed theory value
- (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
- Otherwise the theory becomes stale!
+ \item \verb|Context.>>|~\isa{f} applies context transformation
+ \isa{f} to the implicit context of the {\ML} toplevel.
\end{description}