diff -r ec0fb01c6d50 -r 95c3ae4baba8 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Library/Order_Continuity.thy	Sat Oct 01 17:16:35 2016 +0200
@@ -123,7 +123,7 @@
       case (Suc i)
       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
-      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
+      also have "\<dots> = lfp F" by (simp add: lfp_fixpoint[OF mono])
       finally show ?case .
     qed simp
   qed
@@ -287,7 +287,7 @@
     fix i show "gfp F \<le> (F ^^ i) top"
     proof (induct i)
       case (Suc i)
-      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
+      have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
       also have "\<dots> = (F ^^ Suc i) top" by simp
       finally show ?case .