# HG changeset patch
# User blanchet
# Date 1448885696 -3600
# Node ID 6af17b2b773d33a60f4526e3b9b39a3b09b9de82
# Parent  862daa8144f337d264198c91fcd11f504791f474
removed tracing

diff -r 862daa8144f3 -r 6af17b2b773d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Nov 29 19:01:54 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 30 13:14:56 2015 +0100
@@ -1491,13 +1491,10 @@
 
 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
   let
-    val _ = trace_msg ctxt (fn () => "Extracting clasimpset...")
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val ctxt = ctxt |> Config.put instantiate_inducts false
-    val _ = trace_msg ctxt (fn () => "Extracting facts...")
     val facts =
       nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
-      |> tap (fn _ => trace_msg ctxt (fn () => "Sorting facts..."))
       |> sort (crude_thm_ord ctxt o apply2 snd o swap)
     val num_facts = length facts
     val prover = hd provers
@@ -1505,7 +1502,6 @@
     fun learn auto_level run_prover =
       mash_learn_facts ctxt params prover auto_level run_prover one_year facts
       |> writeln
-    val _ = trace_msg ctxt (fn () => "MaShing...")
   in
     if run_prover then
       (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^