make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 02 22:03:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 02 22:15:20 2010 +0200
@@ -409,15 +409,15 @@
       0 => priority "No subgoal!"
     | n =>
       let
+        val thy = Proof.theory_of state
         val timer = Timer.startRealTimer ()
         val _ = () |> not blocking ? kill_atps
         val _ = priority "Sledgehammering..."
+        val provers = map (`(get_prover thy)) atps
         fun run () =
           let
             val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
-            val thy = Proof.theory_of state
             val (_, hyp_ts, concl_t) = strip_subgoal goal i
-            val provers = map (`(get_prover thy)) atps
             val max_max_relevant =
               case max_relevant of
                 SOME n => n