--- a/src/HOL/Tools/res_atp_provers.ML Thu Apr 27 12:09:32 2006 +0200
+++ b/src/HOL/Tools/res_atp_provers.ML Thu Apr 27 12:10:47 2006 +0200
@@ -13,11 +13,9 @@
fun if_proof_E instr =
let val thisLine = TextIO.inputLine instr
- in
- if thisLine = "# Proof found!\n"
- then true
- else if (thisLine = "") then false
- else if_proof_E instr end;
+ in thisLine <> "" andalso
+ (thisLine = "# Proof found!\n" orelse if_proof_E instr)
+ end;
local
@@ -30,7 +28,8 @@
let val _ = location file
val runtime = "-t " ^ (string_of_int time)
val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
- val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,file])
+ val ch:(TextIO.instream,TextIO.outstream) Unix.proc =
+ Unix.execute(vampire, [runtime,file])
val (instr,outstr) = Unix.streamsOf ch
in if_proof_vampire instr
end;
@@ -39,19 +38,23 @@
let val _ = location file
val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
val runtime = "--cpu-limit=" ^ (string_of_int time)
- val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file])
+ val ch:(TextIO.instream,TextIO.outstream) Unix.proc =
+ Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file])
val (instr,outstr) = Unix.streamsOf ch
in if_proof_E instr
end;
end
-fun vampire_o thy (file,time) = (if (call_vampire (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const)
- else (ResAtp.cond_rm_tmp file;raise Fail ("vampire oracle failed")));
+fun vampire_o _ (file,time) =
+ if call_vampire (file,time)
+ then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+ else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
-
-fun eprover_o thy (file,time) = (if (call_eprover (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const)
- else (ResAtp.cond_rm_tmp file;raise Fail ("eprover oracle failed")));
+fun eprover_o _ (file,time) =
+ if call_eprover (file,time)
+ then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+ else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
end;