less verbose -- the warning will reach the users anyway by other means
authorblanchet
Wed, 31 Oct 2012 11:23:21 +0100
changeset 49991 e0761153fbd1
parent 49990 42209bfa1548
child 49992 1e68f4701906
less verbose -- the warning will reach the users anyway by other means
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