src/HOL/Tools/res_atp_provers.ML
changeset 18726 02b310b1fa10
parent 18272 4f0904ba19c2
child 19129 b66dff8ab7e9
     1.1 --- a/src/HOL/Tools/res_atp_provers.ML	Fri Jan 20 04:35:23 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp_provers.ML	Fri Jan 20 04:50:01 2006 +0100
     1.3 @@ -19,6 +19,13 @@
     1.4    else if (thisLine = "") then false
     1.5    else if_proof_E instr end;		
     1.6  
     1.7 +local 
     1.8 +
     1.9 +fun locations [] = ()
    1.10 +|   locations (s::ss) = (warning s; locations ss);
    1.11 +
    1.12 +in 
    1.13 +
    1.14  fun call_vampire (files:string list, time: int) = 
    1.15    let val output = (space_implode " " files) ^ "  "
    1.16        val runtime = "-t " ^ (string_of_int time)
    1.17 @@ -37,7 +44,7 @@
    1.18    in if_proof_E instr
    1.19    end; 
    1.20  
    1.21 -
    1.22 +end
    1.23  
    1.24  fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
    1.25    else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));