# HG changeset patch
# User blanchet
# Date 1321462798 -3600
# Node ID 43ca06e6c16818cda0ea3d3744573550d1dc858e
# Parent  741f308c0f363ee91b57e68fd3e66129ad9d610f
compile

diff -r 741f308c0f36 -r 43ca06e6c168 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- 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)
diff -r 741f308c0f36 -r 43ca06e6c168 src/HOL/TPTP/CASC_Setup.thy
--- 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