# HG changeset patch
# User desharna
# Date 1642849509 -3600
# Node ID 8dc52ba4155b6f8ef943625e8f2c50e5c673d90b
# Parent  f21e7e6172a0175b77aac05950669566d87e126a
tuned trivial check in mirabelle_sledgehammer

diff -r f21e7e6172a0 -r 8dc52ba4155b src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Jan 22 11:46:25 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Jan 22 12:05:09 2022 +0100
@@ -438,7 +438,7 @@
       #> not trivial ? inc_proof_method_nontriv_calls)
   end
 
-val try_timeout = seconds 5.0
+val try0 = Try0.try0 (SOME (Time.fromSeconds 5)) ([], [], [], [])
 
 fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
   let
@@ -470,9 +470,7 @@
           ""
         else
           let
-            val trivial =
-              check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre
-              handle Timeout.TIMEOUT _ => false
+            val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false
             val (outcome, log1, change_data1, proof_method_and_used_thms) =
               run_sledgehammer params output_dir e_selection_heuristic term_order
                 force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre