diff -r c48becd96398 -r a7664ca9ffc5 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Dec 14 18:52:17 2016 +0100 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Thu Dec 15 15:05:35 2016 +0100 @@ -22,6 +22,7 @@ (* ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *} +ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} 20 "$TPTP/Problems/SYO/SYO304^5.p" *} *) end