--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Nov 07 17:56:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Nov 07 18:02:02 2010 +0100
@@ -425,6 +425,9 @@
val {outcome, used_facts, run_time_in_msecs} =
TimeLimit.timeLimit timeout
(SMT_Solver.smt_filter remote timeout state facts) i
+ handle TimeLimit.TimeOut =>
+ {outcome = SOME SMT_Solver.Time_Out, used_facts = [],
+ run_time_in_msecs = NONE}
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
val too_many_facts_perhaps =