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;
authorwenzelm
Sat Jan 19 22:17:26 2013 +0100 (2013-01-19)
changeset 50987616789281413
parent 50986 c54ea7f5418f
child 50988 5231bfb8bfcf
child 50989 a7f6ce0493b7
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;
src/Pure/goal.ML
     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;