depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);

--- 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));