# HG changeset patch
# User wenzelm
# Date 1481731181 -3600
# Node ID 7141a3a4dc835e424e534c0d4d5c1a1133ddeab2
# Parent  679710d324f134a563ddedfb6c90644669f8567e
always close derivation, for significantly improved performance without parallel proofs;

diff -r 679710d324f1 -r 7141a3a4dc83 src/Pure/Isar/proof.ML
--- 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);
diff -r 679710d324f1 -r 7141a3a4dc83 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Dec 14 15:48:18 2016 +0100
+++ b/src/Pure/goal.ML	Wed Dec 14 16:59:41 2016 +0100
@@ -232,7 +232,7 @@
           (Thm.term_of stmt);
   in
     res
-    |> length props > 1 ? Thm.close_derivation
+    |> Thm.close_derivation
     |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt