--- a/src/Pure/Isar/proof.ML Wed Dec 14 15:48:18 2016 +0100
+++ b/src/Pure/Isar/proof.ML Wed Dec 14 16:59:41 2016 +0100
@@ -522,8 +522,7 @@
fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
val th =
- (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
- handle THM _ => err_lost ())
+ (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
|> Drule.flexflex_unique (SOME ctxt)
|> Thm.check_shyps ctxt
|> Thm.check_hyps (Context.Proof ctxt);