src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     fun default_prover_name () =
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
       handle List.Empty => error "No ATP available."
     fun get_prover name =
       (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
-                Sledgehammer_Provers.Normal (K ()) name)
+                Sledgehammer_Provers.Normal (K (K ())) name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
     | NONE => get_prover (default_prover_name ()))
   end

        ("preplay_timeout", preplay_timeout)]
       |> sh_minimizeLST (*don't confuse the two minimization flags*)
       |> max_new_mono_instancesLST
       |> max_mono_itersLST)
     val minimize =
-      Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
+      Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
     val (used_facts, (preplay, message, message_tail)) =
       minimize st (these (!named_thms))
     val msg = message (preplay ()) ^ message_tail