prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 14:00:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 14:08:30 2010 +0200
@@ -363,6 +363,8 @@
             in
               prover params (minimize_command name) problem |> #message
               handle ERROR message => "Error: " ^ message ^ "\n"
+                   | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
+                            "\n"
             end)
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 14:00:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 09 14:08:30 2010 +0200
@@ -535,8 +535,8 @@
 val dangerous_types = [@{type_name unit}, @{type_name bool}];
 
 (* Facts containing variables of type "unit" or "bool" or of the form
-   "!x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are
-   omitted. *)
+   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
+   are omitted. *)
 fun is_dangerous_term _ @{prop True} = true
   | is_dangerous_term full_types t =
     not full_types andalso