--- a/src/HOL/Tools/atp_wrapper.ML Fri Apr 03 18:03:29 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Sat Apr 04 20:22:39 2009 +0200
@@ -102,7 +102,7 @@
(ResAtp.get_relevant max_new theory_const goal n)
(ResAtp.write_problem_file false)
command
- ResReconstruct.find_failure_e_vamp_spass
+ ResReconstruct.find_failure
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
timeout n goal;
@@ -166,7 +166,7 @@
(ResAtp.write_problem_file true)
(Path.explode "$SPASS_HOME/SPASS",
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
- ResReconstruct.find_failure_e_vamp_spass
+ ResReconstruct.find_failure
ResReconstruct.lemma_list_dfg
timeout n goal;