src/Pure/Isar/proof.ML
changeset 64567 7141a3a4dc83
parent 64420 2efc128370fa
child 65458 cf504b7a7aa7
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Dec 14 15:48:18 2016 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Dec 14 16:59:41 2016 +0100
     1.3 @@ -522,8 +522,7 @@
     1.4      fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
     1.5  
     1.6      val th =
     1.7 -      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
     1.8 -        handle THM _ => err_lost ())
     1.9 +      (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
    1.10        |> Drule.flexflex_unique (SOME ctxt)
    1.11        |> Thm.check_shyps ctxt
    1.12        |> Thm.check_hyps (Context.Proof ctxt);