# HG changeset patch
# User paulson
# Date 1148912311 -7200
# Node ID 73aab222fecbd231399d1a16d4fe7659559e26a8
# Parent  0843210d3756863267edc15caaabda490c512ce4
Giving the "--silent" switch to E, to produce less output

diff -r 0843210d3756 -r 73aab222fecb src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon May 29 13:15:53 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon May 29 16:18:31 2006 +0200
@@ -388,7 +388,7 @@
 	       let val Eprover = helper_path "E_HOME" "eproof"
 	       in
 		  ("E", Eprover, 
-		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time, probfile) ::
+		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
 		   make_atp_list xs (n+1)
 	       end
 	     else error ("Invalid prover name: " ^ !prover)