src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 57056 8b2283566f6e
parent 57054 fed0329ea8e2
child 57154 f0eff6393a32
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu May 22 04:12:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu May 22 05:23:50 2014 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4       message_tail : string}
     1.5  
     1.6    type prover =
     1.7 -    params -> ((string * string list) list -> string -> minimize_command)
     1.8 -    -> prover_problem -> prover_result
     1.9 +    params -> ((string * string list) list -> string -> minimize_command) -> prover_problem ->
    1.10 +    prover_result
    1.11  
    1.12    val SledgehammerN : string
    1.13    val str_of_mode : mode -> string
    1.14 @@ -76,8 +76,7 @@
    1.15    val is_atp : theory -> string -> bool
    1.16    val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    1.17    val is_fact_chained : (('a * stature) * 'b) -> bool
    1.18 -  val filter_used_facts :
    1.19 -    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    1.20 +  val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    1.21      ((''a * stature) * 'b) list
    1.22    val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
    1.23      Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
    1.24 @@ -294,8 +293,7 @@
    1.25        sort_strings (SMT2_Config.available_solvers_of ctxt)
    1.26        |> List.partition (String.isPrefix remote_prefix)
    1.27    in
    1.28 -    Output.urgent_message ("Supported provers: " ^
    1.29 -                           commas (local_provers @ remote_provers) ^ ".")
    1.30 +    Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
    1.31    end
    1.32  
    1.33  fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"