# HG changeset patch
# User wenzelm
# Date 1321025132 -3600
# Node ID 5b5d3ee2285b6fb6ad5f9ad8c2272f6454f51f47
# Parent  615ba724b2696bde948ad5ca98dc1b7f4137ab19
depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);

diff -r 615ba724b269 -r 5b5d3ee2285b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Nov 11 16:06:26 2011 +0100
+++ b/src/Pure/goal.ML	Fri Nov 11 16:25:32 2011 +0100
@@ -125,7 +125,7 @@
       val _ = forked 1;
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = 0, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));