always close derivation, for significantly improved performance without parallel proofs;

--- 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);

--- 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