diff -r 5bc908e5bf42 -r a91d126338a4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 23 14:12:21 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 23 14:12:22 2014 +0200
@@ -151,7 +151,6 @@
           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_preprocess ctxt [] goal weighted_facts i