tuned signature;

--- a/src/Pure/goal.ML	Sat Oct 13 00:08:36 2012 +0200
+++ b/src/Pure/goal.ML	Sat Oct 13 16:19:16 2012 +0200
@@ -21,7 +21,7 @@
   val init: cterm -> thm
   val protect: thm -> thm
   val conclude: thm -> thm
-  val check_finished: Proof.context -> thm -> unit
+  val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
   val fork_name: string -> (unit -> 'a) -> 'a future
@@ -85,7 +85,7 @@
 *)
 fun check_finished ctxt th =
   (case Thm.nprems_of th of
-    0 => ()
+    0 => th
   | n => raise THM ("Proof failed.\n" ^
       Pretty.string_of (Pretty.chunks
         (Goal_Display.pretty_goals
@@ -94,7 +94,7 @@
             |> Config.put Goal_Display.show_main_goal true) th)) ^
       "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
 
-fun finish ctxt th = (check_finished ctxt th; conclude th);
+fun finish ctxt = check_finished ctxt #> conclude;
 
 
 

--- a/src/Pure/subgoal.ML	Sat Oct 13 00:08:36 2012 +0200
+++ b/src/Pure/subgoal.ML	Sat Oct 13 16:19:16 2012 +0200
@@ -140,7 +140,7 @@
 val FOCUS_PREMS = GEN_FOCUS (true, false);
 val FOCUS = GEN_FOCUS (true, true);
 
-fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt;
+fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
 
 end;