diff -r c06f1d36a8c9 -r dedd7952a62c src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Jun 27 20:09:39 2013 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Thu Jun 27 23:17:26 2013 +0200
@@ -13,7 +13,7 @@
 
 ML_file "sledgehammer_tactics.ML"
 
-ML {* Proofterm.proofs := 0 *}
+declare [[proofs = 0]]
 
 declare [[show_consts]] (* for Refute *)
 declare [[smt_oracle]]