# HG changeset patch
# User wenzelm
# Date 1169208997 -3600
# Node ID bc8aee017f8a7fea1b5ee7224284dce59998589d
# Parent  d9b614dc883d751874de82047e38f2f1bbca9cbf
adapted ML context operations;

diff -r d9b614dc883d -r bc8aee017f8a doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 13:09:37 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Fri Jan 19 13:16:37 2007 +0100
@@ -301,18 +301,12 @@
 %
 \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
diff -r d9b614dc883d -r bc8aee017f8a doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:09:37 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 13:16:37 2007 +0100
@@ -240,18 +240,12 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML context: "theory -> unit"} \\
   @{index_ML the_context: "unit -> theory"} \\
   @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML context}~@{text thy} sets the {\ML} theory context to
-  @{text 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 @{ML "the_context ()"} refers to the theory context of the
   {\ML} toplevel --- at compile time!  {\ML} code needs to take care
   to refer to @{ML "the_context ()"} correctly.  Recall that
diff -r d9b614dc883d -r bc8aee017f8a doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri Jan 19 13:09:37 2007 +0100
+++ b/doc-src/antiquote_setup.ML	Fri Jan 19 13:16:37 2007 +0100
@@ -30,7 +30,7 @@
         then txt1 ^ " = " ^ txt2
         else txt1 ^ ": " ^ txt2;
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
-    val _ = Context.use_mltext (ml (txt1, txt2)) false (SOME (ProofContext.theory_of ctxt));
+    val _ = Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
   in
     "\\indexml" ^ kind ^ enclose "{" "}"
       (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^