# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID 576bd30cc4ea4c69d8b89ff0b3931471c265cf48
# Parent  a4b654185613108d5dfa4395b936f922d389ffbf
clearer SystemOnTPTP errors

diff -r a4b654185613 -r 576bd30cc4ea src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
@@ -360,13 +360,15 @@
 fun get_system name versions =
   Synchronized.change_result systems
       (fn systems => (if null systems then get_systems () else systems)
-                     |> `(find_system name versions))
+                     |> `(`(find_system name versions)))
 
 fun the_system name versions =
   case get_system name versions of
-    SOME sys => sys
-  | NONE => error ("System " ^ quote name ^
-                   " is not available at SystemOnTPTP.")
+    (SOME sys, _) => sys
+  | (NONE, []) => error ("SystemOnTPTP is currently not available.")
+  | (NONE, 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 *)