--- a/src/HOL/TPTP/atp_problem_import.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu Apr 18 17:07:01 2013 +0200
@@ -234,7 +234,7 @@
SOLVE_TIMEOUT (timeout div 20) "nitpick"
(nitpick_finite_oracle_tac ctxt (timeout div 20) i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
- (asm_full_simp_tac (simpset_of ctxt) i)
+ (asm_full_simp_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
(auto_tac ctxt