--- 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" ^