# HG changeset patch
# User desharna
# Date 1642778262 -3600
# Node ID fe14ceff1cfdf09339cf0660f853d54518e149b8
# Parent  d4a52993a81e56a20b5437d5b1ad32fb49620c07
added syping of fact filtering time to sledgehammer

diff -r d4a52993a81e -r fe14ceff1cfd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 21 15:38:00 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 21 16:17:42 2022 +0100
@@ -330,15 +330,18 @@
               | NONE =>
                 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
                   |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
-            val _ = spying spy (fn () => (state, i, "All",
-              "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
+            val ({elapsed, ...}, factss) = Timing.timing
+              (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
+              all_facts
+            val () = spying spy (fn () => (state, i, "All",
+              "Filtering " ^ string_of_int (length all_facts) ^ " facts in " ^
+              string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^
               str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
+            val () = if verbose then print (string_of_factss factss) else ()
+            val () = spying spy (fn () =>
+              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))
           in
-            all_facts
-            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
-            |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
-            |> spy ? tap (fn factss => spying spy (fn () =>
-              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+            factss
           end
 
         fun launch_provers () =