1.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:09:37 2007 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:16:37 2007 +0100
     1.3 @@ -240,18 +240,12 @@
     1.4  
     1.5  text %mlref {*
     1.6    \begin{mldecls}
     1.7 -  @{index_ML context: "theory -> unit"} \\
     1.8    @{index_ML the_context: "unit -> theory"} \\
     1.9    @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
    1.10    \end{mldecls}
    1.11  
    1.12    \begin{description}
    1.13  
    1.14 -  \item @{ML context}~@{text thy} sets the {\ML} theory context to
    1.15 -  @{text thy}.  This is usually performed automatically by the system,
    1.16 -  when dropping out of the interactive Isar toplevel into {\ML}, or
    1.17 -  when Isar invokes {\ML} to process code from a string or a file.
    1.18 -
    1.19    \item @{ML "the_context ()"} refers to the theory context of the
    1.20    {\ML} toplevel --- at compile time!  {\ML} code needs to take care
    1.21    to refer to @{ML "the_context ()"} correctly.  Recall that