src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_atp, names) =>
         let
-          fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
+          fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
             | get_thms (name, loc) =
               SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in
           change_data id inc_sh_success;
           if trivial then () else change_data id inc_sh_nontriv_success;