src/HOL/Tools/Sledgehammer/sledgehammer.ML

 signature SLEDGEHAMMER =
 sig
   type failure = ATP_Systems.failure
   type locality = Sledgehammer_Filter.locality
   type relevance_override = Sledgehammer_Filter.relevance_override
+  type fol_formula = Sledgehammer_Translate.fol_formula
   type minimize_command = Sledgehammer_Reconstruct.minimize_command
   type params =
     {blocking: bool,
      debug: bool,
      verbose: bool,

      expect: string}
   type problem =
     {ctxt: Proof.context,
      goal: thm,
      subgoal: int,
-     axioms: ((string * locality) * thm) list}
+     axiom_ts: term list,
+     prepared_axioms: ((string * locality) * fol_formula) option list}
   type prover_result =
     {outcome: failure option,
      message: string,
      pool: string Symtab.table,
      used_thm_names: (string * locality) list,

 
 type problem =
   {ctxt: Proof.context,
    goal: thm,
    subgoal: int,
-   axioms: ((string * locality) * thm) list}
+   axiom_ts: term list,
+   prepared_axioms: ((string * locality) * fol_formula) option list}
 
 type prover_result =
   {outcome: failure option,
    message: string,
    pool: string Symtab.table,

         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
          known_failures, default_max_relevant, explicit_forall,
          use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
-        minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
+        minimize_command
+        ({ctxt, goal, subgoal, axiom_ts, prepared_axioms} : problem) =
   let
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val max_relevant = the_default default_max_relevant max_relevant
-    val axioms = take max_relevant axioms
+    val axiom_ts = take max_relevant axiom_ts
+    val prepared_axioms = take max_relevant prepared_axioms
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                        else Config.get ctxt dest_dir
     val the_problem_prefix = Config.get ctxt problem_prefix
     val problem_file_name =

                                             known_failures output
               in (output, msecs, proof, outcome) end
             val readable_names = debug andalso overlord
             val (problem, pool, conjecture_offset, axiom_names) =
               prepare_problem ctxt readable_names explicit_forall full_types
-                              explicit_apply hyp_ts concl_t axioms
+                              explicit_apply hyp_ts concl_t axiom_ts
+                              prepared_axioms
             val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
                                               problem
             val _ = File.write_list probfile ss
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1

          ""
        else
          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
     fun run () =
       let
-        val problem = {ctxt = ctxt, goal = goal, subgoal = i, axioms = axioms}
+        val problem =
+          {ctxt = ctxt, goal = goal, subgoal = i,
+           axiom_ts = map (prop_of o snd) axioms,
+           prepared_axioms = map (prepare_axiom ctxt) axioms}
         val (outcome_code, message) =
           prover_fun atp_name prover params (minimize_command atp_name) problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
           handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")