src/HOL/TPTP/ATP_Problem_Import.thy
changeset 52487 48bc24467008
parent 52470 dedd7952a62c
child 57812 8dc9dc241973
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jun 30 11:30:16 2013 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jun 30 11:37:34 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  ML_file "sledgehammer_tactics.ML"
     1.6  
     1.7 -declare [[proofs = 0]]
     1.8 +ML {* Proofterm.proofs := 0 *}
     1.9  
    1.10  declare [[show_consts]] (* for Refute *)
    1.11  declare [[smt_oracle]]