src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 37627 1d1754ccd233
parent 37624 3ee568334813
child 37926 e6ff246c0cdb
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 29 10:36:36 2010 +0200
@@ -33,8 +33,8 @@
      axiom_clauses: ((string * int) * thm) list option,
      filtered_clauses: ((string * int) * thm) list option}
   datatype failure =
-    Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
-    MalformedInput | MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -102,8 +102,8 @@
    filtered_clauses: ((string * int) * thm) list option}
 
 datatype failure =
-  Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
-  MalformedInput | MalformedOutput | UnknownError
+  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+  OldSpass | MalformedInput | MalformedOutput | UnknownError
 
 type prover_result =
   {outcome: failure option,