src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32510 1b56f8b1e5cc
parent 32451 8f0dc876fb1b
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Sep 03 15:47:39 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Sep 03 17:55:31 2009 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    type prover = int -> (thm * (string * int)) list option ->
     1.5      (thm * (string * int)) list option -> string -> int ->
     1.6      Proof.context * (thm list * thm) ->
     1.7 -    bool * (string * string list) * string * string vector * (thm * (string * int)) list
     1.8 +    bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
     1.9    val add_prover: string -> prover -> theory -> theory
    1.10    val print_provers: theory -> unit
    1.11    val get_prover: string -> theory -> prover option
    1.12 @@ -305,7 +305,7 @@
    1.13  type prover = int -> (thm * (string * int)) list option ->
    1.14    (thm * (string * int)) list option -> string -> int ->
    1.15    Proof.context * (thm list * thm) ->
    1.16 -  bool * (string * string list) * string * string vector * (thm * (string * int)) list
    1.17 +  bool * (string * string list) * int * string * string vector * (thm * (string * int)) list
    1.18  
    1.19  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    1.20  
    1.21 @@ -345,7 +345,7 @@
    1.22            let
    1.23              val _ = register birthtime deadtime (Thread.self (), desc)
    1.24              val result =
    1.25 -              let val (success, (message, _), _, _, _) =
    1.26 +              let val (success, (message, _), _, _, _, _) =
    1.27                  prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
    1.28                in (success, message) end
    1.29                handle ResHolClause.TOO_TRIVIAL