diff -r 3029fb2d5650 -r 6c5755ad9cae src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Nov 23 23:05:28 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Nov 24 13:24:30 2006 +0100
@@ -817,7 +817,7 @@
 	       let val Eprover = helper_path "E_HOME" "eproof"
 	       in
 		  ("E", Eprover, 
-		     "--tptp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
+		     "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
 		   make_atp_list xs (n+1)
 	       end
 	     else error ("Invalid prover name: " ^ !prover)