# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID d7a6ad5d27bf3793bfd5dd80966eadfae8c0e86f
# Parent  6435b2c7303812886d96878bc4f2e96e7610be31
don't use aggressive with HO ATP

diff -r 6435b2c73038 -r d7a6ad5d27bf src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -290,11 +290,13 @@
     val (conjs, assms, ctxt) =
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
-    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.vampireN
+    val (last_hope_atp, last_hope_aggressive) =
+      if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
   in
     (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (atp_tac ctxt 2 [] timeout last_hope 1) conj)
+     can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+         (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj)
     |> print_szs_from_success conjs
   end