# HG changeset patch
# User wenzelm
# Date 1564127951 -7200
# Node ID 3c20a86f14f13e8b3595804898fbcd38d06e08e7
# Parent  dc65ea2947365564330545fa7e66276cd8585806
finalize proofs earlier to reduce memory requirement;

diff -r dc65ea294736 -r 3c20a86f14f1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 26 09:50:23 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 26 09:59:11 2019 +0200
@@ -1660,7 +1660,7 @@
     else
       (singleton o Future.forks)
         {name = "Proofterm.fulfill_proof_future", group = NONE,
-          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 1,
           interrupts = true}
         fulfill
   end;