--- 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
--- 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
--- 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";