--- a/src/HOL/ResAtpMethods.thy Tue Mar 07 03:48:02 2006 +0100
+++ b/src/HOL/ResAtpMethods.thy Tue Mar 07 03:49:26 2006 +0100
@@ -7,14 +7,13 @@
theory ResAtpMethods
imports Reconstruction
uses
- "Tools/res_atp_setup.ML"
"Tools/res_atp_provers.ML"
("Tools/res_atp_methods.ML")
begin
-oracle vampire_oracle ("(string list * string list) * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("(string list * string list) * int") = {* ResAtpProvers.eprover_o *}
+oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
use "Tools/res_atp_methods.ML"
setup ResAtpMethods.ResAtps_setup