# HG changeset patch
# User wenzelm
# Date 1256763700 -3600
# Node ID d0c2ef49061392c38a591a9a2ea1a6b2ca2f742d
# Parent  bd3f30da7bc129d7cb30c3283ddd498f4136828f
Isar.goal: Proof.simple_goal, not raw version;

diff -r bd3f30da7bc1 -r d0c2ef490613 src/Pure/System/isar.ML
--- 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 ());