# HG changeset patch
# User wenzelm
# Date 1267739167 -3600
# Node ID 77dfdbf85fb80e1e6ce82ab56beb2382f1557591
# Parent  8fbbfc39508ff56e3030a78459da9035fabebdc6
tuned;

diff -r 8fbbfc39508f -r 77dfdbf85fb8 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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);