--- 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