--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 10:23:31 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 10:31:29 2010 +0100
@@ -480,11 +480,7 @@
else
()
val {outcome, used_facts, run_time_in_msecs} =
- TimeLimit.timeLimit iter_timeout
- (SMT_Solver.smt_filter remote iter_timeout state facts) i
- handle TimeLimit.TimeOut =>
- {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
- run_time_in_msecs = NONE}
+ SMT_Solver.smt_filter remote iter_timeout state facts i
val _ =
if verbose andalso is_some outcome then
"SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)