# HG changeset patch # User wenzelm # Date 981544559 -3600 # Node ID a378479996f7994ae14d6c2d24f5b10be208357f # Parent c1b32e7124b42505a2d1f0dd2bc06db5a437e4da val get_goal: state -> context * (thm list * thm); diff -r c1b32e7124b4 -r a378479996f7 src/Pure/Isar/proof.ML --- 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)) =