# HG changeset patch
# User blanchet
# Date 1281355710 -7200
# Node ID 581a402a80f04662122d98b21a096de4649e3ab8
# Parent  74dd8dd335125a145b64cdce216d177f6dfb4494
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

diff -r 74dd8dd33512 -r 581a402a80f0 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
 
diff -r 74dd8dd33512 -r 581a402a80f0 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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