src/HOL/Tools/res_atp.ML
changeset 17435 0eed5a1c00c1
parent 17422 3b237822985d
child 17484 f6a225f97f0a
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 16 11:38:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 16 11:39:09 2005 +0200
     1.3 @@ -132,11 +132,10 @@
     1.4                end
     1.5              else if !prover = "vampire"
     1.6  	    then 
     1.7 -              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
     1.8 +              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
     1.9                in
    1.10 -                ([("vampire", goalstring, vampire, "-t60%-m100000",
    1.11 -                   probfile)] @
    1.12 -                 (make_atp_list xs (n+1)))
    1.13 +                ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
    1.14 +                 (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.15                end
    1.16        	     else if !prover = "E"
    1.17        	     then