# HG changeset patch
# User wenzelm
# Date 1256828956 -3600
# Node ID 6ca8a7984fd97e97931c5ca3025612776506636d
# Parent  49cd8abb2863c45ca6382300750f0db8729c5deb
unregister: eliminated unused status;

diff -r 49cd8abb2863 -r 6ca8a7984fd9 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:08:45 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:09:16 2009 +0100
@@ -86,7 +86,7 @@
 
 (* unregister ATP thread *)
 
-fun unregister (success, message) thread = Synchronized.change global_state
+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) =>
@@ -149,7 +149,7 @@
         do
           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
             |> these
-            |> List.app (unregister (false, "Interrupted (reached timeout)"));
+            |> List.app (unregister "Interrupted (reached timeout)");
             print_new_messages ();
             (*give threads some time to respond to interrupt*)
             OS.Process.sleep min_wait_time)
@@ -263,14 +263,11 @@
           let
             val _ = register birth_time death_time (Thread.self (), desc);
             val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
-            val result =
-              let val {success, message, ...} = prover (! timeout) problem;
-              in (success, message) end
+            val message = #message (prover (! timeout) problem)
               handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
-                  (true, "Empty clause: Try this command: " ^
-                    Markup.markup Markup.sendback "apply metis")
-                | ERROR msg => (false, "Error: " ^ msg);
-            val _ = unregister result (Thread.self ());
+                  "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+                | ERROR msg => ("Error: " ^ msg);
+            val _ = unregister message (Thread.self ());
           in () end)
       in () end);