# HG changeset patch
# User wenzelm
# Date 1275597119 -7200
# Node ID 2bde06a2a706180020d4f4c9a7ad1413bb08b867
# Parent  9763792e4ac7c503fc2332cdbb21b966f7604e15
discontinued obsolete Isar.context() -- long superseded by @{context};

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
diff -r 9763792e4ac7 -r 2bde06a2a706 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Jun 03 22:17:36 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Jun 03 22:31:59 2010 +0200
@@ -335,7 +335,6 @@
   \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
   \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
   \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
-  \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
   \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
 \verb|  {context: Proof.context, facts: thm list, goal: thm}| \\
   \end{mldecls}
@@ -352,9 +351,6 @@
   toplevel state and error condition, respectively.  This only works
   after having dropped out of the Isar toplevel loop.
 
-  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
-  (\secref{sec:generic-context}).
-
   \item \verb|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
diff -r 9763792e4ac7 -r 2bde06a2a706 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Thu Jun 03 22:17:36 2010 +0200
+++ b/src/Pure/System/isar.ML	Thu Jun 03 22:31:59 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/isar.ML
     Author:     Makarius
 
-The global Isabelle/Isar state and main read-eval-print loop.
+Global state of the raw Isar read-eval-print loop.
 *)
 
 signature ISAR =
@@ -9,7 +9,6 @@
   val init: unit -> unit
   val exn: unit -> (exn * string) option
   val state: unit -> Toplevel.state
-  val context: unit -> Proof.context
   val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
   val print: unit -> unit
   val >> : Toplevel.transition -> bool
@@ -57,9 +56,6 @@
 
 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
 
-fun context () = Toplevel.context_of (state ())
-  handle Toplevel.UNDEF => error "Unknown context";
-
 fun goal () = Proof.goal (Toplevel.proof_of (state ()))
   handle Toplevel.UNDEF => error "No goal present";