src/HOL/Tools/atp_manager.ML
changeset 31752 19a5f1c8a844
parent 31409 d8537ba165b5
child 31791 c9a1caf218c8
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:09 2009 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4    val info: unit -> unit
     1.5    val messages: int option -> unit
     1.6    type prover = int -> (thm * (string * int)) list option ->
     1.7 -    (int Symtab.table * bool Symtab.table) option -> string -> int ->
     1.8 +    (thm * (string * int)) list option -> string -> int ->
     1.9      Proof.context * (thm list * thm) ->
    1.10 -    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.11 +    bool * string * string * string vector * (thm * (string * int)) list
    1.12    val add_prover: string -> prover -> theory -> theory
    1.13    val print_provers: theory -> unit
    1.14    val get_prover: string -> theory -> prover option
    1.15 @@ -292,9 +292,9 @@
    1.16  (* named provers *)
    1.17  
    1.18  type prover = int -> (thm * (string * int)) list option ->
    1.19 -  (int Symtab.table * bool Symtab.table) option -> string -> int ->
    1.20 +  (thm * (string * int)) list option -> string -> int ->
    1.21    Proof.context * (thm list * thm) ->
    1.22 -  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.23 +  bool * string * string * string vector * (thm * (string * int)) list
    1.24  
    1.25  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    1.26