src/Pure/goal.ML
changeset 49845 9b19c0e81166
parent 49830 28d207ba9340
child 49847 ed5080c03165
     1.1 --- a/src/Pure/goal.ML	Sat Oct 13 00:08:36 2012 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat Oct 13 16:19:16 2012 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val init: cterm -> thm
     1.5    val protect: thm -> thm
     1.6    val conclude: thm -> thm
     1.7 -  val check_finished: Proof.context -> thm -> unit
     1.8 +  val check_finished: Proof.context -> thm -> thm
     1.9    val finish: Proof.context -> thm -> thm
    1.10    val norm_result: thm -> thm
    1.11    val fork_name: string -> (unit -> 'a) -> 'a future
    1.12 @@ -85,7 +85,7 @@
    1.13  *)
    1.14  fun check_finished ctxt th =
    1.15    (case Thm.nprems_of th of
    1.16 -    0 => ()
    1.17 +    0 => th
    1.18    | n => raise THM ("Proof failed.\n" ^
    1.19        Pretty.string_of (Pretty.chunks
    1.20          (Goal_Display.pretty_goals
    1.21 @@ -94,7 +94,7 @@
    1.22              |> Config.put Goal_Display.show_main_goal true) th)) ^
    1.23        "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
    1.24  
    1.25 -fun finish ctxt th = (check_finished ctxt th; conclude th);
    1.26 +fun finish ctxt = check_finished ctxt #> conclude;
    1.27  
    1.28  
    1.29