# HG changeset patch
# User wenzelm
# Date 1206731291 -3600
# Node ID aedaf65f7a57ceceb302b636cd2b9106a6a9dc2b
# Parent  9283b4185fdfe719a88eeecc1b3ca7a7361508fe
updated generated file;

diff -r 9283b4185fdf -r aedaf65f7a57 doc-src/IsarImplementation/Thy/document/integration.tex
--- 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}