--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Feb 05 12:27:10 2012 +0100
@@ -356,9 +356,8 @@
(* Experimental *)
val spass_new_config : atp_config =
- {exec = ("ISABELLE_ATP", "scripts/spass_new"),
- required_execs =
- [("SPASS_NEW_HOME", "SPASS"), ("SPASS_NEW_HOME", "tptp2dfg")],
+ {exec = ("SPASS_NEW_HOME", "SPASS"),
+ required_execs = [],
arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
(* TODO: add: -FPDFGProof -FPFCR *)
("-Auto -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
--- a/src/HOL/Tools/ATP/scripts/spass_new Sun Feb 05 12:27:10 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS 3.8 that also outputs the clause-to-formula relation
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-
-rm -f "$name.prf"
-"$SPASS_NEW_HOME/SPASS" $options "$name"
-if [ -f "$name.prf" ]
-then
- cat "$name.prf"
- rm -f "$name.prf"
-fi