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;
1.1 --- a/src/Pure/goal.ML Sat Jan 19 21:05:05 2013 +0100
1.2 +++ b/src/Pure/goal.ML Sat Jan 19 22:17:26 2013 +0100
1.3 @@ -225,6 +225,7 @@
1.4 Thm.strip_shyps);
1.5 val local_result =
1.6 Thm.future global_result global_prop
1.7 + |> Thm.close_derivation
1.8 |> Thm.instantiate (instT, [])
1.9 |> Drule.forall_elim_list fixes
1.10 |> fold (Thm.elim_implies o Thm.assume) assms;