# HG changeset patch
# User blanchet
# Date 1328353698 -3600
# Node ID 8bff5fb211de913e0bd8cd63fc354d5d09c3fd44
# Parent  cafa325419f6f9421a918c2e1f3d988f59494b7f
the new SPASS gives accurate fact information, so no need for old hack anymore

diff -r cafa325419f6 -r 8bff5fb211de src/HOL/Tools/ATP/scripts/spass_new
--- a/src/HOL/Tools/ATP/scripts/spass_new	Sat Feb 04 12:08:18 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass_new	Sat Feb 04 12:08:18 2012 +0100
@@ -8,8 +8,7 @@
 name=${@:$(($#)):1}
 
 rm -f "$name.prf"
-"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options "$name" \
-    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options "$name"
 if [ -f "$name.prf" ]
 then
   cat "$name.prf"