--- a/src/Pure/Concurrent/future.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Mar 03 15:23:02 2016 +0100
@@ -348,7 +348,7 @@
(Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
List.app cancel_later (cancel_all ());
signal work_available; true)
- else reraise exn;
+ else Exn.reraise exn;
fun scheduler_loop () =
(while
@@ -409,8 +409,8 @@
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
- SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
- | _ => reraise exn);
+ SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
+ | _ => Exn.reraise exn);
val ok =
(case the (Single_Assignment.peek result) of
Exn.Exn exn =>
@@ -600,7 +600,7 @@
| exn =>
if Exn.is_interrupt exn
then raise Fail "Concurrent attempt to fulfill promise"
- else reraise exn;
+ else Exn.reraise exn;
fun job () =
Multithreading.with_attributes Multithreading.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));