diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Tue Mar 20 18:42:45 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass	Tue Mar 20 18:42:45 2012 +0100
@@ -7,12 +7,13 @@
 
 options=${@:1:$(($#-1))}
 name=${@:$(($#)):1}
+home=${SPASS_OLD_HOME:-$SPASS_HOME}
 
-"$SPASS_HOME/SPASS" -Flotter "$name" \
+"$home/SPASS" -Flotter "$name" \
     | sed 's/description({$/description({*/' \
     | sed 's/set_ClauseFormulaRelation()\.//' \
     > $name.cnf
 cat $name.cnf
-"$SPASS_HOME/SPASS" $options "$name.cnf" \
+"$home/SPASS" $options "$name.cnf" \
     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
 rm -f "$name.cnf"