# HG changeset patch
# User mengj
# Date 1140695859 -3600
# Node ID 495ecbefc5dfb4f8dd9da6935dcb1953c9dbbe8a
# Parent  9aff3d859d3991fdfff09339c861b922bfb6d750
vampire/eprover methods can now be applied repeatedly until they fail.

diff -r 9aff3d859d39 -r 495ecbefc5df src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Wed Feb 22 22:18:42 2006 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML	Thu Feb 23 12:57:39 2006 +0100
@@ -26,12 +26,12 @@
 
 (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
 fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm =
-    SELECT_GOAL
-	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
+    (SELECT_GOAL
+	(EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
 		  METAHYPS(fn negs =>
 			      HEADGOAL(Tactic.rtac 
 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
-							   (ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) handle Fail _ => no_tac) n thm;
+							   (ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) n thm) handle (Fail _) => Seq.empty;
 
 (* vampire and eprover tactics *)