# HG changeset patch
# User wenzelm
# Date 1358630246 -3600
# Node ID 6167892814138d90e8593f75cf4cbbb95bf75631
# Parent  c54ea7f5418f01bd40ea4407446fb9696b9b6df9
always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;

diff -r c54ea7f5418f -r 616789281413 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jan 19 21:05:05 2013 +0100
+++ b/src/Pure/goal.ML	Sat Jan 19 22:17:26 2013 +0100
@@ -225,6 +225,7 @@
         Thm.strip_shyps);
     val local_result =
       Thm.future global_result global_prop
+      |> Thm.close_derivation
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;