--- a/src/HOL/Tools/res_atp.ML Fri Sep 16 11:38:49 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 16 11:39:09 2005 +0200
@@ -132,11 +132,10 @@
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