src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML

      change_data #> inc_sh_time_isa cpu_time)
   end
 
 end
 
-val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) []
+val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) Try0.empty_facts
 
 fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
   let
     (* Parse Mirabelle-specific parameters *)
     val check_trivial =