# HG changeset patch
# User wenzelm
# Date 1313856677 -7200
# Node ID e10f6b873f88d2d5740abe343772291f2f6c1f13
# Parent  aa9c1e9ef2cec8a532c7f57edbe2bb68b4a740e9
tuned future priorities (again);

diff -r aa9c1e9ef2ce -r e10f6b873f88 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 20 16:06:27 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 18:11:17 2011 +0200
@@ -176,7 +176,7 @@
 fun check_body_thms (body as PBody {thms, ...}) =
   (singleton o Future.cond_forks)
     {name = "Proofterm.check_body_thms", group = NONE,
-      deps = map (Future.task_of o #3 o #2) thms, pri = ~1, interrupts = true}
+      deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
     (fn () => (join_thms thms; body));
 
 fun proof_of (PBody {proof, ...}) = proof;
@@ -1406,7 +1406,7 @@
   | fulfill_proof_future thy promises postproc body =
       (singleton o Future.forks)
         {name = "Proofterm.fulfill_proof_future", group = NONE,
-          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = ~1,
+          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
           interrupts = true}
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1464,7 +1464,7 @@
       else
         (singleton o Future.cond_forks)
           {name = "Proofterm.prepare_thm_proof", group = NONE,
-            deps = [], pri = ~1, interrupts = true}
+            deps = [], pri = 0, interrupts = true}
           (make_body0 o full_proof0);
 
     fun new_prf () =