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