misc tuning: more concise operations on prems (without change of exceptions);
discontinue odd clone Drule.cprems_of (see also 991a3feaf270);
(* Title: HOL/Tools/Mirabelle/mirabelle_metis.ML
Author: Jasmin Blanchette, TU Munich
Author: Sascha Boehme, TU Munich
Author: Martin Desharnais, UniBw Munich
Mirabelle action: "metis".
*)
structure Mirabelle_Metis: MIRABELLE_ACTION =
struct
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
fun run ({pre, post, ...} : Mirabelle.command) =
let
val thms = Mirabelle.theorems_of_sucessful_proof post;
val names = map Thm.get_name_hint thms;
val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre)));
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 (map Thm_Name.short names))
end
in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "metis" make_action
end