--- a/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
for FILE in "$@"
do
- echo "theory $SCRATCH imports \"Main\" begin ML {* Refute.refute_tptp_file \"$FILE\" *} end;" \
+ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \
> /tmp/$SCRATCH.thy
"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done