facilitate debugging

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 17:43:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 18:10:32 2010 +0100
@@ -458,7 +458,7 @@
 val smt_iter_min_msecs = Unsynchronized.ref 5000
 val smt_monomorph_limit = Unsynchronized.ref 4
 
-fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
+fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
   let
     val ctxt = Proof.context_of state
     fun iter timeout iter_num outcome0 time_so_far facts =
@@ -482,6 +482,11 @@
           else
             ()
         val birth = Timer.checkRealTimer timer
+        val _ =
+          if debug then
+            Output.urgent_message "Invoking SMT solver..."
+          else
+            ()
         val {outcome, used_facts, ...} =
           SMT_Solver.smt_filter remote iter_timeout state facts i
         val death = Timer.checkRealTimer timer
@@ -489,6 +494,8 @@
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
             |> Output.urgent_message
+          else if debug then
+            Output.urgent_message "SMT solver returned."
           else
             ()
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 17:43:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 18:10:32 2010 +0100
@@ -180,9 +180,11 @@
                                   | (false, _) => run_prover problem prover)
                    provers (false, state)
             else
-              provers |> (if blocking then Par_List.map else map)
-                             (run_prover problem)
-                      |> exists fst |> rpair state
+              provers
+              |> (if blocking andalso length provers > 1 then Par_List.map
+                  else map)
+                     (run_prover problem)
+              |> exists fst |> rpair state
           end
       val run_atps =
         run_provers "ATP" no_dangerous_types atp_relevance_fudge