src/Pure/Concurrent/future.ML
changeset 56013 d64a4ef26edb
parent 55298 99b9249b3e05
parent 55760 890e983cb07b
child 57675 38f1422ef473
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Dec 05 17:52:12 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Dec 05 17:58:03 2013 +0100
     1.3 @@ -438,7 +438,7 @@
     1.4    Position.setmp_thread_data pos (fn () =>
     1.5      let val id = Position.get_id pos in
     1.6        if is_none id orelse is_none exec_id orelse id = exec_id
     1.7 -      then Output.error_msg' (serial, msg) else ()
     1.8 +      then Output.error_message' (serial, msg) else ()
     1.9      end) ();
    1.10  
    1.11  fun identify_result pos res =