diff -r 989a34fa72b3 -r eeede26f2721 src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Mon May 28 20:25:38 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
-# Isar proof reconstruction)
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-home=${SPASS_OLD_HOME:-$SPASS_HOME}
-
-"$home/SPASS" -Flotter "$name" \
-    | sed 's/description({$/description({*/' \
-    | sed 's/set_ClauseFormulaRelation()\.//' \
-    > $name.cnf
-cat $name.cnf
-"$home/SPASS" $options "$name.cnf" \
-    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f "$name.cnf"