trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

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