# HG changeset patch
# User mengj
# Date 1132294237 -3600
# Node ID 6c63f0eb16d7bd61e16d68b88fa4e8d1e2717061
# Parent  9d476d1054d74eae3d3106924d3573043720697d
-- changed the interface of functions vampire_oracle and eprover_oracle.

diff -r 9d476d1054d7 -r 6c63f0eb16d7 src/HOL/ResAtpMethods.thy
--- a/src/HOL/ResAtpMethods.thy	Fri Nov 18 07:10:00 2005 +0100
+++ b/src/HOL/ResAtpMethods.thy	Fri Nov 18 07:10:37 2005 +0100
@@ -13,8 +13,8 @@
 
 begin
 
-oracle vampire_oracle ("string list * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("string list * int") = {* ResAtpProvers.eprover_o *}
+oracle vampire_oracle ("(string list * string list) * int") = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle ("(string list * string list) * int") = {* ResAtpProvers.eprover_o *}
 
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.ResAtps_setup