1.1 --- a/src/Pure/Concurrent/future.ML	Thu Jan 17 12:04:05 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Jan 17 12:04:52 2013 +0100
     1.3 @@ -439,8 +439,10 @@
     1.4  
     1.5  fun error_msg pos ((serial, msg), exec_id) =
     1.6    Position.setmp_thread_data pos (fn () =>
     1.7 -    if is_none exec_id orelse exec_id = Position.get_id pos
     1.8 -    then Output.error_msg' (serial, msg) else warning msg) ();
     1.9 +    let val id = Position.get_id pos in
    1.10 +      if is_none id orelse is_none exec_id orelse id = exec_id
    1.11 +      then Output.error_msg' (serial, msg) else ()
    1.12 +    end) ();
    1.13  
    1.14  fun identify_result pos res =
    1.15    (case res of