# HG changeset patch
# User wenzelm
# Date 1282056439 -7200
# Node ID 1f51486da674f8467a5d436d42ae14f9c089b43a
# Parent  e0b8b173368995f80c4802964065499f04723970
made 9043eefe8d71 actually compile;

diff -r e0b8b1733689 -r 1f51486da674 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 16:38:45 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 16:47:19 2010 +0200
@@ -8,7 +8,9 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+    OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+    MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,