tuned future priorities (again);
authorwenzelm
Sat Aug 20 18:11:17 2011 +0200 (2011-08-20 ago)
changeset 44332e10f6b873f88
parent 44331 aa9c1e9ef2ce
child 44333 cc53ce50f738
tuned future priorities (again);
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 16:06:27 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat Aug 20 18:11:17 2011 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  fun check_body_thms (body as PBody {thms, ...}) =
     1.5    (singleton o Future.cond_forks)
     1.6      {name = "Proofterm.check_body_thms", group = NONE,
     1.7 -      deps = map (Future.task_of o #3 o #2) thms, pri = ~1, interrupts = true}
     1.8 +      deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
     1.9      (fn () => (join_thms thms; body));
    1.10  
    1.11  fun proof_of (PBody {proof, ...}) = proof;
    1.12 @@ -1406,7 +1406,7 @@
    1.13    | fulfill_proof_future thy promises postproc body =
    1.14        (singleton o Future.forks)
    1.15          {name = "Proofterm.fulfill_proof_future", group = NONE,
    1.16 -          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = ~1,
    1.17 +          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
    1.18            interrupts = true}
    1.19          (fn () =>
    1.20            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    1.21 @@ -1464,7 +1464,7 @@
    1.22        else
    1.23          (singleton o Future.cond_forks)
    1.24            {name = "Proofterm.prepare_thm_proof", group = NONE,
    1.25 -            deps = [], pri = ~1, interrupts = true}
    1.26 +            deps = [], pri = 0, interrupts = true}
    1.27            (make_body0 o full_proof0);
    1.28  
    1.29      fun new_prf () =