ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 17:51:25 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 17:56:07 2010 +0100
@@ -420,8 +420,11 @@
 fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
   let
     val timer = Timer.startRealTimer ()
+    (* The "timeout" argument passed to "smt_filter" is a soft timeout. We make
+       it hard using "timeLimit". *)
     val {outcome, used_facts, run_time_in_msecs} =
-      SMT_Solver.smt_filter remote timeout state facts i
+      TimeLimit.timeLimit timeout
+                          (SMT_Solver.smt_filter remote timeout state facts) i
     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 =