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;

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