src/HOL/IMP/Abs_Int0.thy

--- a/src/HOL/IMP/Abs_Int0.thy	Sat Nov 08 16:35:24 2014 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Nov 08 16:42:04 2014 +0100
@@ -130,7 +130,7 @@
 
 lemma pfp_inv:
   "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
-unfolding pfp_def by (metis (lifting) while_option_rule)
+unfolding pfp_def by (erule while_option_rule [rotated])
 
 lemma strip_pfp:
 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"