src/HOL/Tools/Sledgehammer/sledgehammer.ML

      isar_proof: bool,
      isar_shrink_factor: int,
      timeout: Time.time,
      expect: string}
 
-  type atp_problem =
+  datatype axiom =
+    Unprepared of (string * locality) * thm |
+    Prepared of term * ((string * locality) * fol_formula) option
+
+  type prover_problem =
     {state: Proof.state,
      goal: thm,
      subgoal: int,
-     axioms: (term * ((string * locality) * fol_formula) option) list,
+     axioms: axiom list,
      only: bool}
 
-  type atp_result =
+  type prover_result =
     {outcome: failure option,
      message: string,
-     pool: string Symtab.table,
-     used_thm_names: (string * locality) list,
-     atp_run_time_in_msecs: int,
-     output: string,
-     tstplike_proof: string,
-     axiom_names: (string * locality) list vector,
-     conjecture_shape: int list list}
-
-  type atp = params -> minimize_command -> atp_problem -> atp_result
+     used_axioms: (string * locality) list,
+     run_time_in_msecs: int}
+
+  type prover = params -> minimize_command -> prover_problem -> prover_result
 
   val smtN : string
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
   val available_provers : theory -> unit
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val run_atp : theory -> string -> atp
+  val run_atp : theory -> string -> prover
+  val is_smt_solver_installed : unit -> bool
   val run_smt_solver :
-    Proof.context -> bool -> Time.time -> ('a * thm) list -> string * 'a list
-  val is_smt_solver_installed : unit -> bool
+    bool -> params -> minimize_command -> prover_problem
+    -> string * (string * locality) list
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
   val setup : theory -> theory
 end;

    isar_proof: bool,
    isar_shrink_factor: int,
    timeout: Time.time,
    expect: string}
 
-type atp_problem =
+datatype axiom =
+  Unprepared of (string * locality) * thm |
+  Prepared of term * ((string * locality) * fol_formula) option
+
+type prover_problem =
   {state: Proof.state,
    goal: thm,
    subgoal: int,
-   axioms: (term * ((string * locality) * fol_formula) option) list,
+   axioms: axiom list,
    only: bool}
 
-type atp_result =
+type prover_result =
   {outcome: failure option,
    message: string,
-   pool: string Symtab.table,
-   used_thm_names: (string * locality) list,
-   atp_run_time_in_msecs: int,
-   output: string,
-   tstplike_proof: string,
-   axiom_names: (string * locality) list vector,
-   conjecture_shape: int list list}
-
-type atp = params -> minimize_command -> atp_problem -> atp_result
+   used_axioms: (string * locality) list,
+   run_time_in_msecs: int}
+
+type prover = params -> minimize_command -> prover_problem -> prover_result
 
 (* configuration attributes *)
 
 val (dest_dir, dest_dir_setup) =
   Attrib.config_string "sledgehammer_dest_dir" (K "")

 fun proof_banner auto =
   if auto then "Sledgehammer found a proof" else "Try this command"
 
 (* generic TPTP-based ATPs *)
 
+fun dest_Unprepared (Unprepared p) = p
+  | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
+fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
+  | prepared_axiom _ (Prepared p) = p
+
 (* Important messages are important but not so important that users want to see
    them each time. *)
 val important_message_keep_factor = 0.1
 
 fun atp_fun auto atp_name
         {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 ({state, goal, subgoal, axioms, only} : atp_problem) =
+        minimize_command
+        ({state, goal, subgoal, axioms, only} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
-    val axioms = axioms |> not only
-                          ? take (the_default default_max_relevant max_relevant)
+    val axioms =
+      axioms |> not only ? take (the_default default_max_relevant max_relevant)
+             |> map (prepared_axiom ctxt)
     val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                    else Config.get ctxt dest_dir
     val problem_prefix = Config.get ctxt problem_prefix
-    val atp_problem_file_name =
+    val problem_file_name =
       Path.basic ((if overlord then "prob_" ^ atp_name
                    else problem_prefix ^ serial_string ())
                   ^ "_" ^ string_of_int subgoal)
-    val atp_problem_path_name =
+    val problem_path_name =
       if dest_dir = "" then
-        File.tmp_path atp_problem_file_name
+        File.tmp_path problem_file_name
       else if File.exists (Path.explode dest_dir) then
-        Path.append (Path.explode dest_dir) atp_problem_file_name
+        Path.append (Path.explode dest_dir) problem_file_name
       else
         error ("No such directory: " ^ quote dest_dir ^ ".")
     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     (* write out problem file and call ATP *)

         ()
       else
         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
     val ((pool, conjecture_shape, axiom_names),
          (output, msecs, tstplike_proof, outcome)) =
-      with_path cleanup export run_on atp_problem_path_name
+      with_path cleanup export run_on problem_path_name
     val (conjecture_shape, axiom_names) =
       repair_conjecture_shape_and_axiom_names output conjecture_shape
                                               axiom_names
     val important_message =
       if random () <= important_message_keep_factor then
         extract_important_message output
       else
         ""
-    val (message, used_thm_names) =
+    val (message, used_axioms) =
       case outcome of
         NONE =>
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
             (proof_banner auto, full_types, minimize_command, tstplike_proof,

                    important_message
                  else
                    ""))
       | SOME failure => (string_for_failure failure, [])
   in
-    {outcome = outcome, message = message, pool = pool,
-     used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
-     output = output, tstplike_proof = tstplike_proof,
-     axiom_names = axiom_names, conjecture_shape = conjecture_shape}
+    {outcome = outcome, message = message, used_axioms = used_axioms,
+     run_time_in_msecs = msecs}
   end
 
 fun run_atp thy name = atp_fun false name (get_atp thy name)
 
 fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
                                 expect, ...})
                     auto i n minimize_command
-                    (atp_problem as {state, goal, axioms, ...})
-                    (atp as {default_max_relevant, ...}, atp_name) =
+                    (prover_problem as {state, goal, axioms, ...})
+                    (prover as {default_max_relevant, ...}, atp_name) =
   let
     val ctxt = Proof.context_of state
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val max_relevant = the_default default_max_relevant max_relevant
     val num_axioms = Int.min (length axioms, max_relevant)
     val desc = prover_description ctxt params atp_name num_axioms i n goal
     fun go () =
       let
         fun really_go () =
-          atp_fun auto atp_name atp params (minimize_command atp_name)
-                  atp_problem
+          atp_fun auto atp_name prover params (minimize_command atp_name)
+                  prover_problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
         val (outcome_code, message) =
           if debug then
             really_go ()

       (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
        (false, state))
   end
 
 (* FIXME: dummy *)
-fun run_smt_solver ctxt remote timeout axioms =
+fun is_smt_solver_installed () = true
+
+(* FIXME: dummy *)
+fun raw_run_smt_solver remote timeout state axioms i =
   ("", axioms |> take 5 |> map fst)
 
-(* FIXME: dummy *)
-fun is_smt_solver_installed () = true
-
-fun run_smt_solver_somehow ctxt (params as {timeout, ...}) i n goal axioms
+fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+                   ({state, subgoal, axioms, ...} : prover_problem) =
+  raw_run_smt_solver remote timeout state
+                     (map_filter (try dest_Unprepared) axioms) subgoal
+
+fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms
                            (remote, name) =
   let
-    val desc =
-      prover_description ctxt params name (length axioms) i n goal
-    val (failure, used_thm_names) = run_smt_solver ctxt remote timeout axioms
+    val ctxt = Proof.context_of state
+    val desc = prover_description ctxt params name (length axioms) i n goal
+    val (failure, used_axioms) =
+      raw_run_smt_solver remote timeout state axioms i
     val success = (failure = "")
     val message =
       das_Tool ^ ": " ^ desc ^ "\n" ^
       (if success then
          sendback_line (proof_banner false)
                        (apply_on_subgoal i n ^
-                        command_call "smt" (map fst used_thm_names))
+                        command_call "smt" (map fst used_axioms))
        else
          "Error: " ^ failure)
   in priority message; success end
 
 val smt_default_max_relevant = 300 (* FUDGE *)

                   |> auto ? (fn n => n div auto_max_relevant_divisor)
             val axioms =
               relevant_facts ctxt full_types relevance_thresholds
                              max_max_relevant relevance_override chained_ths
                              hyp_ts concl_t
-            val atp_problem =
+            val prover_problem =
               {state = state, goal = goal, subgoal = i,
-               axioms = map (prepare_axiom ctxt) axioms, only = only}
+               axioms = axioms |> map (Prepared o prepare_axiom ctxt),
+               only = only}
             val run_atp_somehow =
-              run_atp_somehow params auto i n minimize_command atp_problem
+              run_atp_somehow params auto i n minimize_command prover_problem
           in
             if auto then
-              fold (fn atp => fn (true, state) => (true, state)
-                               | (false, _) => run_atp_somehow atp)
+              fold (fn prover => fn (true, state) => (true, state)
+                                  | (false, _) => run_atp_somehow prover)
                    atps (false, state)
             else
               atps |> (if blocking then Par_List.map else map) run_atp_somehow
                    |> exists fst |> rpair state
           end

             val axioms =
               relevant_facts ctxt full_types relevance_thresholds
                              max_relevant relevance_override chained_ths
                              hyp_ts concl_t
           in
-            smts |> map (run_smt_solver_somehow ctxt params i n goal axioms)
+            smts |> map (run_smt_solver_somehow state params i n goal axioms)
                  |> exists I |> rpair state
           end
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smt_solvers]
         |> Par_List.map (fn f => f (false, state) |> K ())