diff -r 9763792e4ac7 -r 2bde06a2a706 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jun 03 22:17:36 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jun 03 22:31:59 2010 +0200
@@ -274,7 +274,6 @@
   @{index_ML Isar.loop: "unit -> unit"} \\
   @{index_ML Isar.state: "unit -> Toplevel.state"} \\
   @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
-  @{index_ML Isar.context: "unit -> Proof.context"} \\
   @{index_ML Isar.goal: "unit ->
   {context: Proof.context, facts: thm list, goal: thm}"} \\
   \end{mldecls}
@@ -291,10 +290,6 @@
   toplevel state and error condition, respectively.  This only works
   after having dropped out of the Isar toplevel loop.
 
-  \item @{ML "Isar.context ()"} produces the proof context from @{ML
-  "Isar.state ()"}, analogous to @{ML Context.proof_of}
-  (\secref{sec:generic-context}).
-
   \item @{ML "Isar.goal ()"} produces the full Isar goal state,
   consisting of proof context, facts that have been indicated for
   immediate use, and the tactical goal according to