# HG changeset patch
# User blanchet
# Date 1274084214 -7200
# Node ID 67ae217c6b5c6eae783710c24f8adf1426c1dbcf
# Parent  ef698bd61057c3ee67607b32ae8267fcc53ae1b6
identify common SPASS error more clearly

diff -r ef698bd61057 -r 67ae217c6b5c src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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,
diff -r ef698bd61057 -r 67ae217c6b5c src/HOL/Tools/ATP_Manager/atp_systems.ML
--- 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