changeset 46365 | 547d1a1dcaf6 |
parent 46320 | 0b8b73b49848 |
child 47790 | 2e1636e45770 |
--- a/src/HOL/TPTP/CASC_Setup.thy Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/TPTP/CASC_Setup.thy Mon Jan 30 17:15:59 2012 +0100 @@ -129,7 +129,7 @@ Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" - (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt [])) + (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) ORELSE