diff -r e4a3f9c3d4f5 -r 511e6976f031 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 29 23:19:26 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 30 00:17:06 2009 +0200
@@ -30,6 +30,7 @@
   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
@@ -311,6 +312,10 @@
   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 **)