src/HOL/Tools/atp_wrapper.ML
changeset 30151 629f3a92863e
parent 30016 76b58a07e704
child 30242 aea5d7fa7ef5
--- a/src/HOL/Tools/atp_wrapper.ML	Wed Feb 25 10:02:10 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Thu Feb 26 10:13:43 2009 +0100
@@ -96,7 +96,7 @@
 
 fun tptp_prover_opts_full max_new theory_const full command =
   external_prover
-    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
+    (ResAtp.write_problem_files false max_new theory_const)
     command
     ResReconstruct.find_failure_e_vamp_spass
     (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
@@ -153,7 +153,7 @@
 (* SPASS *)
 
 fun spass_opts max_new theory_const = external_prover
-  (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
+  (ResAtp.write_problem_files true max_new theory_const)
   (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
   ResReconstruct.find_failure_e_vamp_spass
   ResReconstruct.lemma_list_dfg;