src/HOL/Tools/Mirabelle/mirabelle_metis.ML

         fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts);
       in
         (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
         |> not (null names) ? suffix (":\n" ^ commas names)
       end
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "metis" make_action
 
 end