more thorough Lazy.is_finished;

--- a/src/Pure/Concurrent/lazy.ML	Sun Dec 28 15:42:34 2014 +1100
+++ b/src/Pure/Concurrent/lazy.ML	Sun Dec 28 12:18:01 2014 +0100
@@ -36,11 +36,15 @@
     Expr _ => NONE
   | Result res => Future.peek res);
 
+fun is_finished (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => false
+  | Result res =>
+      Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
+
 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
-fun is_finished x = is_some (peek x);
-
 
 (* force result *)