src/HOL/Tools/res_atp_provers.ML

     Author:     Jia Meng, NICTA
 
 Functions used for ATP Oracle.
 *)
 
-
 structure ResAtpProvers =
-
 struct
 
 fun seek_line s instr =
-  let val thisLine = TextIO.inputLine instr
-  in thisLine <> "" andalso 
-     (thisLine = s orelse seek_line s instr) 
-  end;
+  (case TextIO.inputLine instr of
+    NONE => false
+  | SOME thisLine => thisLine = s orelse seek_line s instr);
 
 fun location s = warning ("ATP input at: " ^ s);
 
-fun call_vampire (file:string, time: int) = 
+fun call_vampire (file:string, time: int) =
   let val _ = location file
       val runtime = "-t " ^ (string_of_int time)
       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
       val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file]))
   in seek_line "--------------------- PROVED ----------------------\n" instr

 
 fun call_eprover (file:string, time:int) =
   let val _ = location file
       val eprover = ResAtp.helper_path "E_HOME" "eprover"
       val runtime = "--cpu-limit=" ^ (string_of_int time)
-      val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover, 
+      val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover,
                               [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
   in seek_line "# Proof found!\n" instr
-  end; 
+  end;
 
 fun call_spass (file:string, time:int) =
   let val _ = location file
       val runtime = "-TimeLimit=" ^ (string_of_int time)
       val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
-      val (instr,outstr) = Unix.streamsOf (Unix.execute(spass, 
+      val (instr,outstr) = Unix.streamsOf (Unix.execute(spass,
 			      [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
   in seek_line "SPASS beiseite: Proof found.\n" instr
   end;
 
-fun vampire_o _ (file,time) = 
-  if call_vampire (file,time) 
-  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)  
+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 _ (file,time) = 
-  if call_eprover (file,time) 
+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"));
 
 fun spass_o _ (file,time) =
-    if call_spass (file,time)
-    then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
-    else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
-
+  if call_spass (file,time)
+  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
+  else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
 
 end;
-