src/HOL/Tools/Sledgehammer/sledgehammer.ML

   val measure_runtime : bool Config.T
   val kill_atps: unit -> unit
   val running_atps: unit -> unit
   val messages: int option -> unit
   val get_prover_fun : theory -> string -> prover
-  val start_prover_thread :
-    params -> int -> int -> relevance_override -> (string -> minimize_command)
-    -> Proof.state -> string -> unit
+  val run_sledgehammer :
+    params -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> unit
   val setup : theory -> theory
 end;
 
 structure Sledgehammer : SLEDGEHAMMER =
 struct

      filtered_clauses = the_filtered_clauses}
   end
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-(* start prover thread *)
 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
                         relevance_override minimize_command proof_state name =
   let
     val thy = Proof.theory_of proof_state
     val birth_time = Time.now ()

               prover params (minimize_command name) timeout problem |> #message
               handle ERROR message => "Error: " ^ message ^ "\n"
             end)
   end
 
+fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
+  | run_sledgehammer (params as {atps, ...}) i relevance_override
+                     minimize_command state =
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      let
+        val _ = kill_atps ()
+        val _ = priority "Sledgehammering..."
+        val _ = app (start_prover_thread params i n relevance_override
+                                         minimize_command state) atps
+      in () end
+
 val setup =
   dest_dir_setup
   #> problem_prefix_setup
   #> measure_runtime_setup