src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

   val smt_weight_curve : (int -> int) Unsynchronized.ref
   val smt_max_slices : int Config.T
   val smt_slice_fact_frac : real Config.T
   val smt_slice_time_frac : real Config.T
   val smt_slice_min_secs : int Config.T
-  val das_tool : string
+  val SledgehammerN : string
   val plain_metis : reconstructor
   val select_smt_solver : string -> Proof.context -> Proof.context
   val extract_reconstructor :
     params -> reconstructor -> string * (string * string list) list
   val is_reconstructor : string -> bool

 
 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
-val das_tool = "Sledgehammer"
+val SledgehammerN = "Sledgehammer"
 
 val reconstructor_names = [metisN, smtN]
 val plain_metis = Metis (hd partial_type_encs, combsN)
 val is_reconstructor = member (op =) reconstructor_names
 

   in
     Output.urgent_message ("Supported provers: " ^
                            commas (local_provers @ remote_provers) ^ ".")
   end
 
-fun kill_provers () = Async_Manager.kill_threads das_tool "prover"
-fun running_provers () = Async_Manager.running_threads das_tool "prover"
-val messages = Async_Manager.thread_messages das_tool "prover"
+fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
+fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
+val messages = Async_Manager.thread_messages SledgehammerN "prover"
 
 
 (** problems, results, ATPs, etc. **)
 
 type params =