src/HOL/Tools/ATP_Manager/atp_manager.ML

 (* unregister ATP thread *)
 
 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;
           val message' = description ^ "\n" ^ message;
           val messages' = message' :: messages;

             val message = #message (prover (! timeout) problem)
               handle Res_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
                   "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);
 
 
 (* sledghammer for first subgoal *)