1.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 13:09:37 2007 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 13:16:37 2007 +0100
     1.3 @@ -301,18 +301,12 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{mldecls}
     1.7 -  \indexml{context}\verb|context: theory -> unit| \\
     1.8    \indexml{the-context}\verb|the_context: unit -> theory| \\
     1.9    \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
    1.10    \end{mldecls}
    1.11  
    1.12    \begin{description}
    1.13  
    1.14 -  \item \verb|context|~\isa{thy} sets the {\ML} theory context to
    1.15 -  \isa{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 \verb|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 \verb|the_context ()| correctly.  Recall that

     2.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:09:37 2007 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:16:37 2007 +0100
     2.3 @@ -240,18 +240,12 @@
     2.4  
     2.5  text %mlref {*
     2.6    \begin{mldecls}
     2.7 -  @{index_ML context: "theory -> unit"} \\
     2.8    @{index_ML the_context: "unit -> theory"} \\
     2.9    @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
    2.10    \end{mldecls}
    2.11  
    2.12    \begin{description}
    2.13  
    2.14 -  \item @{ML context}~@{text thy} sets the {\ML} theory context to
    2.15 -  @{text thy}.  This is usually performed automatically by the system,
    2.16 -  when dropping out of the interactive Isar toplevel into {\ML}, or
    2.17 -  when Isar invokes {\ML} to process code from a string or a file.
    2.18 -
    2.19    \item @{ML "the_context ()"} refers to the theory context of the
    2.20    {\ML} toplevel --- at compile time!  {\ML} code needs to take care
    2.21    to refer to @{ML "the_context ()"} correctly.  Recall that

     3.1 --- a/doc-src/antiquote_setup.ML	Fri Jan 19 13:09:37 2007 +0100
     3.2 +++ b/doc-src/antiquote_setup.ML	Fri Jan 19 13:16:37 2007 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4          then txt1 ^ " = " ^ txt2
     3.5          else txt1 ^ ": " ^ txt2;
     3.6      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     3.7 -    val _ = Context.use_mltext (ml (txt1, txt2)) false (SOME (ProofContext.theory_of ctxt));
     3.8 +    val _ = Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
     3.9    in
    3.10      "\\indexml" ^ kind ^ enclose "{" "}"
    3.11        (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^