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