# HG changeset patch
# User paulson
# Date 1192721637 -7200
# Node ID aa9db4e3cd5e7c518cb52d16119a3ef329336236
# Parent  30ce1e078b728794b23d451b8282fcc2bfe99a88
Ensured that the right number of ATP calls is generated

diff -r 30ce1e078b72 -r aa9db4e3cd5e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Oct 18 16:09:39 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Oct 18 17:33:57 2007 +0200
@@ -689,41 +689,28 @@
 (***************************************************************)
 
 (* call prover with settings and problem file for the current subgoal *)
-fun watcher_call_provers sign sg_terms (childin, childout, pid) =
-  let
-    fun make_atp_list [] n = []
-      | make_atp_list (sg_term::xs) n =
-          let
-            val probfile = prob_pathname n
-            val time = Int.toString (!time_limit)
-          in
-            Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
-            (*options are separated by Watcher.setting_sep, currently #"%"*)
-            case !prover of
-                Recon.SPASS =>
+fun watcher_call_provers files (childin, childout, pid) =
+  let val time = Int.toString (!time_limit)
+      fun make_atp_list [] = []
+	| make_atp_list (file::files) =
+	   (Output.debug (fn () => "problem file in watcher_call_provers is " ^ file);
+	    (*options are separated by Watcher.setting_sep, currently #"%"*)
+	    case !prover of
+		Recon.SPASS =>
 		  let val spass = helper_path "SPASS_HOME" "SPASS"
 		      val sopts =
        "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
-		  in
-		      ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
-		  end
-              | Recon.Vampire =>
+		  in  ("spass", spass, sopts, file) :: make_atp_list files  end
+	      | Recon.Vampire =>
 		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
 		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
-		  in
-		      ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
-		  end
-              | Recon.E =>
+		  in  ("vampire", vampire, vopts, file) :: make_atp_list files  end
+	      | Recon.E =>
 		  let val eproof = helper_path "E_HOME" "eproof"
-                      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
-		  in
-		     ("E", eproof, eopts, probfile) :: make_atp_list xs (n+1)
-		  end
-          end
-
-    val atp_list = make_atp_list sg_terms 1
+		      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
+		  in  ("E", eproof, eopts, file) :: make_atp_list files  end)
   in
-    Watcher.callResProvers(childout,atp_list);
+    Watcher.callResProvers(childout, make_atp_list files);
     Output.debug (fn () => "Sent commands to watcher!")
   end
 
@@ -812,7 +799,7 @@
       last_watcher_pid := SOME (childin, childout, pid, files);
       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
       Output.debug (fn () => "pid: " ^ string_of_pid pid);
-      watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid)
+      watcher_call_provers files (childin, childout, pid)
     end;
 
 (*For ML scripts, and primarily, for debugging*)