--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 13 16:40:06 2012 +0100
@@ -62,7 +62,7 @@
fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
- val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
+ val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end