src/HOL/Tools/res_atp.ML

                      optionline, probfile)] @ 
                   (make_atp_list xs (n+1)))
               end
             else if !prover = "vampire"
 	    then 
-              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
+              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
               in
-                ([("vampire", goalstring, vampire, "-t60%-m100000",
-                   probfile)] @
-                 (make_atp_list xs (n+1)))
+                ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
+                 (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
               end
       	     else if !prover = "E"
       	     then
 	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
 	       in