# HG changeset patch
# User blanchet
# Date 1280135997 -7200
# Node ID 586130f71c78665d19cf8c4a6fcb7b5a5fecbcf9
# Parent  ca3041b0f4459ef53d5f8f764fef6706e114d59f
remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)

diff -r ca3041b0f445 -r 586130f71c78 src/HOL/Tools/ATP_Manager/SPASS_TPTP
--- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Mon Jul 26 11:19:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Mon Jul 26 11:19:57 2010 +0200
@@ -14,5 +14,6 @@
     > $name.cnf.dfg
 rm -f $name.fof.dfg
 cat $name.cnf.dfg
-$SPASS_HOME/SPASS $options $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
 rm -f $name.cnf.dfg