diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/lib/Tools/tptp_refute --- a/src/HOL/TPTP/lib/Tools/tptp_refute Fri Apr 27 15:24:37 2012 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute Fri Apr 27 15:24:37 2012 +0200 @@ -26,7 +26,7 @@ for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.refute_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" done