src/Pure/goal.ML

 sig
   include BASIC_GOAL
   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
   val fork: (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list

   --- (finish)
    C
 *)
 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
           (ctxt
             |> Config.put Goal_Display.goals_limit n
             |> 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;
 
 
 
 (** results **)