src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32947 3c19b98a35cd
parent 32941 72d48e333b77
child 32948 e95a4be101a8
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 17:04:45 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 17:06:19 2009 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val messages: int option -> unit
     1.5    val add_prover: string * ATP_Wrapper.prover -> theory -> theory
     1.6    val print_provers: theory -> unit
     1.7 -  val get_prover: string -> theory -> ATP_Wrapper.prover option
     1.8 +  val get_prover: theory -> string -> ATP_Wrapper.prover option
     1.9    val sledgehammer: string list -> Proof.state -> unit
    1.10  end;
    1.11  
    1.12 @@ -302,7 +302,7 @@
    1.13  fun print_provers thy = Pretty.writeln
    1.14    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
    1.15  
    1.16 -fun get_prover name thy =
    1.17 +fun get_prover thy name =
    1.18    (case Symtab.lookup (Provers.get thy) name of
    1.19      NONE => NONE
    1.20    | SOME (prover, _) => SOME prover);
    1.21 @@ -311,7 +311,7 @@
    1.22  (* start prover thread *)
    1.23  
    1.24  fun start_prover name birthtime deadtime i proof_state =
    1.25 -  (case get_prover name (Proof.theory_of proof_state) of
    1.26 +  (case get_prover (Proof.theory_of proof_state) name of
    1.27      NONE => warning ("Unknown external prover: " ^ quote name)
    1.28    | SOME prover =>
    1.29        let