# HG changeset patch
# User blanchet
# Date 1292438484 -3600
# Node ID a99bc6f3664b230b5e667d83225fa99bd1ba8b26
# Parent  5391d34b0f4c1107a25b870294234be8f9f37912
make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)

diff -r 5391d34b0f4c -r a99bc6f3664b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 18:45:14 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 19:41:24 2010 +0100
@@ -193,6 +193,7 @@
         run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
+        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
     in
       (false, state)
       |> (if blocking then run_atps #> not auto ? run_smts