# HG changeset patch
# User paulson
# Date 1146132647 -7200
# Node ID caaf68a64ac420d73f469aed3a0f027a2a05f540
# Parent  25778eacbe219dd779ed3c42da6f2488895c28df
cosmetic changes

diff -r 25778eacbe21 -r caaf68a64ac4 src/HOL/Tools/res_atp_provers.ML
--- 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;