diff -r da05ce2de5a8 -r 8e3891309a8e src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -79,7 +79,8 @@
         else case term_of ct of
           Abs _ =>
           Conv.abs_conv (conv false o snd) ctxt ct
-          |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI})
+          |> wrap
+             ? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
         | _ => Conv.comb_conv (conv true ctxt) ct
       val eqth = conv true ctxt (cprop_of th)
     in Thm.equal_elim eqth th end