diff -r abab10d1f4a3 -r 547d1a1dcaf6 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/IMP/Live_True.thy	Mon Jan 30 17:15:59 2012 +0100
@@ -146,7 +146,7 @@
 lemma while_option_stop2:
  "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
 apply(simp add: while_option_def split: if_splits)
-by (metis (lam_lifting) LeastI_ex)
+by (metis (lifting) LeastI_ex)
 (* move to While_Combinator *)
 lemma while_option_finite_subset_Some: fixes C :: "'a set"
   assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"