# HG changeset patch
# User blanchet
# Date 1283458520 -7200
# Node ID d08fdb351345448c125785112a4bbd73d93b5bab
# Parent  0a62f8a94af3ee64a0635273edf1e6d1c1fd2811
make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

diff -r 0a62f8a94af3 -r d08fdb351345 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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