--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Mar 04 21:10:25 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Mar 04 22:46:07 2010 +0100
@@ -89,7 +89,7 @@
fun unregister message thread = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
- SOME (birth_time, _, description) =>
+ SOME (_, _, description) =>
let
val active' = delete_thread thread active;
val cancelling' = (thread, (Time.now (), description)) :: cancelling;
@@ -267,7 +267,7 @@
"Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
- in () end)
+ in () end);
in () end);