src/HOL/Complete_Partial_Order.thy

--- a/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -293,7 +293,7 @@
 end
 
 instance complete_lattice \<subseteq> ccpo
-  by default (fast intro: Sup_upper Sup_least)+
+  by standard (fast intro: Sup_upper Sup_least)+
 
 lemma lfp_eq_fixp:
   assumes f: "mono f" shows "lfp f = fixp f"