# HG changeset patch
# User wenzelm
# Date 1415461324 -3600
# Node ID 79684150ed6ad8dcc881cbeb6438f287f60a6a59
# Parent  3bf80312508e95b961e9864a3102ec0267a43dc9
avoid slow metis proof;

diff -r 3bf80312508e -r 79684150ed6a 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"