src/Pure/System/isar.ML
changeset 37306 2bde06a2a706
parent 37239 54b444874be1
child 38138 dc65ed8bbb43
     1.1 --- a/src/Pure/System/isar.ML	Thu Jun 03 22:17:36 2010 +0200
     1.2 +++ b/src/Pure/System/isar.ML	Thu Jun 03 22:31:59 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/System/isar.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -The global Isabelle/Isar state and main read-eval-print loop.
     1.8 +Global state of the raw Isar read-eval-print loop.
     1.9  *)
    1.10  
    1.11  signature ISAR =
    1.12 @@ -9,7 +9,6 @@
    1.13    val init: unit -> unit
    1.14    val exn: unit -> (exn * string) option
    1.15    val state: unit -> Toplevel.state
    1.16 -  val context: unit -> Proof.context
    1.17    val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    1.18    val print: unit -> unit
    1.19    val >> : Toplevel.transition -> bool
    1.20 @@ -57,9 +56,6 @@
    1.21  
    1.22  fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    1.23  
    1.24 -fun context () = Toplevel.context_of (state ())
    1.25 -  handle Toplevel.UNDEF => error "Unknown context";
    1.26 -
    1.27  fun goal () = Proof.goal (Toplevel.proof_of (state ()))
    1.28    handle Toplevel.UNDEF => error "No goal present";
    1.29