--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Nov 16 13:08:52 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Nov 16 14:27:10 2015 +0100
@@ -1491,10 +1491,13 @@
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
@@ -1502,6 +1505,7 @@
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" ^