--- a/src/Pure/System/isar.ML Wed Oct 28 22:01:05 2009 +0100
+++ b/src/Pure/System/isar.ML Wed Oct 28 22:01:40 2009 +0100
@@ -10,7 +10,7 @@
val exn: unit -> (exn * string) option
val state: unit -> Toplevel.state
val context: unit -> Proof.context
- val goal: unit -> thm
+ val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
val print: unit -> unit
val >> : Toplevel.transition -> bool
val >>> : Toplevel.transition list -> unit
@@ -60,7 +60,7 @@
fun context () = Toplevel.context_of (state ())
handle Toplevel.UNDEF => error "Unknown context";
-fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
+fun goal () = Proof.goal (Toplevel.proof_of (state ()))
handle Toplevel.UNDEF => error "No goal present";
fun print () = Toplevel.print_state false (state ());