src/HOL/HOLCF/Pcpo.thy

 class chfin = po +
   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
 begin
 
 subclass cpo
-apply default
+apply standard
 apply (frule chfin)
 apply (blast intro: lub_finch1)
 done
 
 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"

 class flat = pcpo +
   assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
 begin
 
 subclass chfin
-apply default
+apply standard
 apply (unfold max_in_chain_def)
 apply (case_tac "\<forall>i. Y i = \<bottom>")
 apply simp
 apply simp
 apply (erule exE)