src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

   type params =
     {debug : bool,
      verbose : bool,
      overlord : bool,
      spy : bool,
-     blocking : bool,
      provers : string list,
      type_enc : string option,
      strict : bool,
      lam_trans : string option,
      uncurried_aliases : bool option,

   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
     Proof.context
-
   val supported_provers : Proof.context -> unit
-  val kill_provers : unit -> unit
-  val running_provers : unit -> unit
-  val messages : int option -> unit
 end;
 
 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
 struct
 

 type params =
   {debug : bool,
    verbose : bool,
    overlord : bool,
    spy : bool,
-   blocking : bool,
    provers : string list,
    type_enc : string option,
    strict : bool,
    lam_trans : string option,
    uncurried_aliases : bool option,

       |> List.partition (String.isPrefix remote_prefix)
   in
     writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
   end
 
-fun kill_provers () = Async_Manager_Legacy.kill_threads SledgehammerN "prover"
-fun running_provers () = Async_Manager_Legacy.running_threads SledgehammerN "prover"
-val messages = Async_Manager_Legacy.thread_messages SledgehammerN "prover"
-
 end;