src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

      max_proofs : int,
      isar_proofs : bool option,
      compress : real option,
      try0 : bool,
      smt_proofs : bool,
+     suggest_of : bool option,
      minimize : bool,
      slices : int,
      timeout : Time.time,
      preplay_timeout : Time.time,
      expect : string}

     {outcome : atp_failure option,
      used_facts : (string * stature) list,
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
+     message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
 
   type prover = params -> prover_problem -> prover_slice -> prover_result
 
   val SledgehammerN : string
   val default_abduce_max_candidates : int
   val str_of_mode : mode -> string
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
   val is_atp : string -> bool
-  val bunches_of_proof_methods : Proof.context -> bool -> bool -> string -> proof_method list list
+  val bunches_of_metis_methods : Proof.context -> bool -> bool -> proof_method list list
+  val bunches_of_smt_methods : Proof.context -> proof_method list list
+  val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> proof_method list list
   val facts_of_filter : string -> (string * fact list) list -> fact list
   val facts_of_basic_slice : base_slice -> (string * fact list) list -> fact list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list

 open ATP_Proof
 open ATP_Util
 open ATP_Problem
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
-open Metis_Tactic
 open Sledgehammer_Fact
 open Sledgehammer_Proof_Methods
 open Sledgehammer_ATP_Systems
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)

    max_proofs : int,
    isar_proofs : bool option,
    compress : real option,
    try0 : bool,
    smt_proofs : bool,
+   suggest_of : bool option,
    minimize : bool,
    slices : int,
    timeout : Time.time,
    preplay_timeout : Time.time,
    expect : string}

   {outcome : atp_failure option,
    used_facts : (string * stature) list,
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
+   message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
 
 type prover = params -> prover_problem -> prover_slice -> prover_result
 
 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
 
 fun proof_banner mode prover_name =
   (case mode of
-    Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
-  | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
-  | _ => "Try this: ")
-
-fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans =
+    Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof:"
+  | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof:"
+  | _ => "Try this:")
+
+fun bunches_of_metis_methods ctxt needs_full_types needs_lam_defs =
+  let
+    (* metis without options (preferred) *)
+    val preferred_method = Metis_Method (NONE, NONE, [])
+
+    (* metis with different options *)
+    val desperate_lam_trans = if needs_lam_defs then liftingN else opaque_liftingN
+    val option_methods =
+      Metis_Method (SOME full_typesN, NONE, []) ::
+      Metis_Method (NONE, SOME liftingN, []) ::
+      Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans, []) ::
+       (if needs_full_types then
+          [Metis_Method (SOME really_full_type_enc, NONE, []),
+           Metis_Method (SOME full_typesN, SOME desperate_lam_trans, [])]
+        else
+          [Metis_Method (SOME no_typesN, SOME desperate_lam_trans, [])])
+
+    (* metis with extensionality (often needed for lifting) *)
+    val ext_facts = [short_thm_name ctxt ext]
+    val ext_methods =
+      Metis_Method (NONE, SOME liftingN, ext_facts) ::
+       (if not needs_lam_defs then
+          []
+        else if needs_full_types then
+          [Metis_Method (SOME full_typesN, SOME liftingN, ext_facts)]
+        else
+          [Metis_Method (SOME no_typesN, SOME liftingN, ext_facts)])
+  in
+    [[preferred_method], option_methods, ext_methods]
+  end
+
+fun bunches_of_smt_methods ctxt =
+  [map (SMT_Method o SMT_Verit) (Verit_Strategies.all_veriT_stgies (Context.Proof ctxt)),
+   [SMT_Method SMT_Z3]]
+
+fun bunches_of_proof_methods ctxt smt_proofs needs_full_types needs_lam_defs =
   let
     val misc_methodss =
       [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
-        Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
+        Metis_Method (NONE, NONE, []), Fastforce_Method, Force_Method, Presburger_Method,
         Argo_Method, Order_Method]]
 
     val metis_methodss =
-      [Metis_Method (SOME full_typesN, NONE) ::
-       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
-       (if needs_full_types then
-          [Metis_Method (SOME really_full_type_enc, NONE),
-           Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
-        else
-          [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])]
+      tl (bunches_of_metis_methods ctxt needs_full_types needs_lam_defs)
 
     val smt_methodss =
       if smt_proofs then
-        [map (SMT_Method o SMT_Verit) (Verit_Strategies.all_veriT_stgies (Context.Proof ctxt)),
-         [SMT_Method SMT_Z3]]
+        bunches_of_smt_methods ctxt
       else
         []
   in
     misc_methodss @ metis_methodss @ smt_methodss
   end