val get_goal: state -> context * (thm list * thm);

--- a/src/Pure/Isar/proof.ML	Tue Feb 06 18:41:27 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Feb 07 12:15:59 2001 +0100
@@ -28,6 +28,7 @@
   val reset_thms: string -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
+  val get_goal: state -> context * (thm list * thm)
   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   val reset_facts: state -> state
@@ -249,6 +250,10 @@
     | find _ (state as State (_, [])) = err_malformed "find_goal" state;
 in val find_goal = find 0 end;
 
+fun get_goal state =
+  let val (ctxt, (_, ((_, x), _))) = find_goal state
+  in (ctxt, x) end;
+
 fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
 
 fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =