diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -62,8 +62,8 @@
  apply (rule idealI)
    apply (cut_tac idealD1 [OF ideal_A], fast)
   apply (clarify, rename_tac i j)
-  apply (drule subsetD [OF chain_A [OF le_maxI1]])
-  apply (drule subsetD [OF chain_A [OF le_maxI2]])
+  apply (drule subsetD [OF chain_A [OF max.cobounded1]])
+  apply (drule subsetD [OF chain_A [OF max.cobounded2]])
   apply (drule (1) idealD2 [OF ideal_A])
   apply blast
  apply clarify