src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

 val strict_default = "false"
 val stride_default = 1
 val max_facts_default = "smart"
 val slice_default = "true"
 val max_calls_default = 10000000
-val trivial_default = "false"
+val check_trivial_default = false
 
 (*If a key is present in args then augment a list with its pair*)
 (*This is used to avoid fixing default values at the Mirabelle level, and
   instead use the default values of the tool (Sledgehammer in this case).*)
 fun available_parameter args key label list =

 
 fun sledgehammer_action args =
   let
     val stride = Mirabelle.get_int_setting args (strideK, stride_default)
     val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default)
+    val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default)
   in
     fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) =>
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
         if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
           ()

               let
                 val meth = Unsynchronized.ref ""
                 val named_thms =
                   Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
                 val trivial =
-                  if AList.lookup (op =) args check_trivialK |> the_default trivial_default
-                                  |> Value.parse_bool then
+                  if check_trivial then
                     Try0.try0 (SOME try_timeout) ([], [], [], []) pre
                     handle Timeout.TIMEOUT _ => false
                   else false
                 fun apply_method () =
                   (Mirabelle.catch_result (proof_method_tag meth) false