# HG changeset patch
# User blanchet
# Date 1329242313 -3600
# Node ID 24990fae5f920f2faed44bef2c481388552d7253
# Parent  837f79bdd3c4a20294fc14a302c3eff6296fb4ff
better error message

diff -r 837f79bdd3c4 -r 24990fae5f92 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 14 17:59:10 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 14 18:58:33 2012 +0100
@@ -493,10 +493,15 @@
 fun the_system name versions =
   case get_system name versions of
     (SOME sys, _) => sys
-  | (NONE, []) => error ("SystemOnTPTP is currently not available.")
+  | (NONE, []) => error ("SystemOnTPTP is not available.")
   | (NONE, syss) =>
-    error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
-           "(Available systems: " ^ commas_quote syss ^ ".)")
+    case syss |> filter_out (String.isPrefix "%")
+              |> filter_out (curry (op =) "") of
+      [] => error ("SystemOnTPTP is not available.")
+    | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
+    | syss =>
+      error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
+             "(Available systems: " ^ commas_quote syss ^ ".)")
 
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)