--- 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,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun May 16 00:02:11 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon May 17 10:16:54 2010 +0200
@@ -100,6 +100,9 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"]))) ^
"\" on a line of its own."
+ | string_for_failure MalformedInput =
+ "Internal Sledgehammer error: The ATP problem is malformed. Please report \
+ \this to the Isabelle developers."
| string_for_failure MalformedOutput = "Error: The ATP output is malformed."
| string_for_failure UnknownError = "Error: An unknown ATP error occurred."
@@ -336,7 +339,8 @@
known_failures =
[(Unprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config