1.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -119,14 +119,16 @@
     1.4     SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
     1.5     ORELSE
     1.6     SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
     1.7 -       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
     1.8 +       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
     1.9 +                      Sledgehammer_Filter.no_relevance_override))
    1.10     ORELSE
    1.11     SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    1.12     ORELSE
    1.13     SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    1.14     ORELSE
    1.15     SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
    1.16 -       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    1.17 +       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
    1.18 +                          Sledgehammer_Filter.no_relevance_override))
    1.19     ORELSE
    1.20     SOLVE_TIMEOUT (max_secs div 10) "metis"
    1.21         (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))