removed noise
authorblanchet
Fri May 23 14:12:22 2014 +0200 (2014-05-23 ago)
changeset 57078a91d126338a4
parent 57077 5bc908e5bf42
child 57079 aa7f051ba6ab
removed noise
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 23 14:12:21 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 23 14:12:22 2014 +0200
     1.3 @@ -151,7 +151,6 @@
     1.4            else
     1.5              ()
     1.6          val birth = Timer.checkRealTimer timer
     1.7 -        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
     1.8  
     1.9          val (outcome, used_facts) =
    1.10            SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 23 14:12:21 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 23 14:12:22 2014 +0200
     2.3 @@ -150,7 +150,6 @@
     2.4            else
     2.5              ()
     2.6          val birth = Timer.checkRealTimer timer
     2.7 -        val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
     2.8  
     2.9          val filter_result as {outcome, ...} =
    2.10            SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout