# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID e0761153fbd160a23f9a9fe6c76b9ab346b79734
# Parent  42209bfa1548ca77ddb19d62332d4666f77e558b
less verbose -- the warning will reach the users anyway by other means

diff -r 42209bfa1548 -r e0761153fbd1 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -590,8 +590,7 @@
           (warning (case extract_known_failure known_perl_failures output of
                       SOME failure => string_for_failure failure
                     | NONE => trim_line output ^ "."); [])) ()
-  handle TimeLimit.TimeOut =>
-         (warning "Cannot retrieve system list from SystemOnTPTP."; [])
+  handle TimeLimit.TimeOut => []
 
 fun find_remote_system name [] systems =
     find_first (String.isPrefix (name ^ "---")) systems