src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 35569 77dfdbf85fb8
parent 33604 d4220df6fde2
child 35592 768d17f54125
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Mar 04 21:10:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Mar 04 22:46:07 2010 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  fun unregister message thread = Synchronized.change global_state
     1.5    (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     1.6      (case lookup_thread active thread of
     1.7 -      SOME (birth_time, _, description) =>
     1.8 +      SOME (_, _, description) =>
     1.9          let
    1.10            val active' = delete_thread thread active;
    1.11            val cancelling' = (thread, (Time.now (), description)) :: cancelling;
    1.12 @@ -267,7 +267,7 @@
    1.13                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    1.14                  | ERROR msg => ("Error: " ^ msg);
    1.15              val _ = unregister message (Thread.self ());
    1.16 -          in () end)
    1.17 +          in () end);
    1.18        in () end);
    1.19  
    1.20