1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 06 12:18:17 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 06 15:21:33 2006 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    structure Isar:
     1.5      sig
     1.6        val state: unit -> Toplevel.state
     1.7 +      val context: unit -> Proof.context
     1.8        val exn: unit -> (exn * string) option
     1.9        val main: unit -> unit
    1.10        val loop: unit -> unit
    1.11 @@ -323,6 +324,7 @@
    1.12  structure Isar =
    1.13  struct
    1.14    val state = Toplevel.get_state;
    1.15 +  val context = Context.proof_of o Toplevel.context_of o state;
    1.16    val exn = Toplevel.exn;
    1.17    fun main () = gen_main false false;
    1.18    fun loop () = gen_loop false false;