Goal.forked: clarified handling of interrupts;

--- a/src/Pure/goal.ML	Wed Aug 10 16:05:14 2011 +0200
+++ b/src/Pure/goal.ML	Wed Aug 10 16:24:39 2011 +0200
@@ -125,12 +125,10 @@
       val _ = forked 1;
       val future =
         singleton
-          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = true})
+          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
           (fn () =>
-            (*interruptible*)
             Exn.release
-              (Exn.capture Future.status e before forked ~1
-                handle exn => (forked ~1; reraise exn)));
+              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
     in future end) ();
 
 fun fork e = fork_name "Goal.fork" e;