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 =