--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun May 16 00:02:11 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 17 10:16:54 2010 +0200
@@ -34,8 +34,8 @@
axiom_clauses: (thm * (string * int)) list option,
filtered_clauses: (thm * (string * int)) list option}
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -95,8 +95,8 @@
filtered_clauses: (thm * (string * int)) list option};
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,