# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID 7b4104df2be628770d80e8599d4a31d2ae196e85
# Parent  99ef9fd7341b010940ab4a8c256c797bac202f78
gracefully handle empty SPASS problems

diff -r 99ef9fd7341b -r 7b4104df2be6 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -290,6 +290,7 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
+      (Unprovable, "No formulae and clauses found in input file"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
diff -r 99ef9fd7341b -r 7b4104df2be6 src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass	Mon Aug 22 15:02:45 2011 +0200
@@ -11,6 +11,7 @@
 "$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
 "$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
     | sed 's/description({$/description({*/' \
+    | sed 's/set_ClauseFormulaRelation()\.//' \
     > $name.cnf.dfg
 rm -f $name.fof.dfg
 cat $name.cnf.dfg