# HG changeset patch
# User wenzelm
# Date 1254265048 -7200
# Node ID 995b9c763c66fb02fed08787006a41fa106cb162
# Parent  c6e6a4665ff5f46e5f89b9bbc3b06e8a77b29b30
replaced chained_goal by slightly more appropriate flat_goal;

diff -r c6e6a4665ff5 -r 995b9c763c66 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 30 00:27:19 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 30 00:57:28 2009 +0200
@@ -30,7 +30,6 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val get_goal: state -> context * (thm list * thm)
-  val chained_goal: state -> context * thm
   val show_main_goal: bool Unsynchronized.ref
   val verbose: bool Unsynchronized.ref
   val pretty_state: int -> state -> Pretty.T list
@@ -38,6 +37,7 @@
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
+  val flat_goal: state -> Proof.context * thm
   val goal_tac: thm -> int -> tactic
   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
   val match_bind: (string list * string) list -> state -> state
@@ -312,10 +312,6 @@
   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   in (ctxt, (using, goal)) end;
 
-fun chained_goal state =
-  let val (ctxt, (using, goal)) = get_goal state
-  in (ctxt, Seq.hd (ALLGOALS (Method.insert_tac using) goal)) end;
-
 
 
 (** pretty_state **)
@@ -441,6 +437,12 @@
 
 end;
 
+fun flat_goal state =
+  let
+    val (_, (using, _)) = get_goal state;
+    val (ctxt, (_, goal)) = get_goal (refine_insert using state);
+  in (ctxt, goal) end;
+
 
 (* refine via sub-proof *)