changeset 45573 | 22d003b5b32e |
parent 44112 | ef876972fdc1 |
child 47529 | 5f35a95c0645 |
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Nov 18 11:47:12 2011 +0100 @@ -203,7 +203,7 @@ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; val _ = if null killing then () - else Output.urgent_message ("Killed active " ^ das_wort_worker ^ "s.") + else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.") in state' end);