avoid erule and rotated in IMP

--- a/src/HOL/IMP/Abs_Int0.thy	Sun Nov 09 10:03:18 2014 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sun Nov 09 11:05:20 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 (erule while_option_rule [rotated])
+unfolding pfp_def by (blast intro: while_option_rule)
 
 lemma strip_pfp:
 assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"