# HG changeset patch
# User blanchet
# Date 1289149322 -3600
# Node ID 1d3df64b1f88bf6cfdf836386f27dffef0321709
# Parent  66c8c1f7e121f13e36bf0dcd099c14d3ed5a4219
catch TimeOut exception

diff -r 66c8c1f7e121 -r 1d3df64b1f88 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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 =