# HG changeset patch
# User blanchet
# Date 1400847142 -7200
# Node ID a91d126338a4fe21618087089d3dfe3fcbd7e8d8
# Parent  5bc908e5bf42d8ea6d1f6d4224bc08e56fb5c8bc
removed noise

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
diff -r 5bc908e5bf42 -r a91d126338a4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 23 14:12:21 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 23 14:12:22 2014 +0200
@@ -150,7 +150,6 @@
           else
             ()
         val birth = Timer.checkRealTimer timer
-        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
 
         val filter_result as {outcome, ...} =
           SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout