--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Nov 16 17:26:42 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Nov 16 17:59:58 2011 +0100
@@ -18,7 +18,8 @@
val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
- fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts)
+ fun metis ctxt =
+ Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
|> prefix (metis_tag id)
--- a/src/HOL/TPTP/CASC_Setup.thy Wed Nov 16 17:26:42 2011 +0100
+++ b/src/HOL/TPTP/CASC_Setup.thy Wed Nov 16 17:59:58 2011 +0100
@@ -131,7 +131,7 @@
Sledgehammer_Filter.no_relevance_override))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
- (ALLGOALS (Metis_Tactic.metis_tac [] ctxt []))
+ (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE