src/HOL/HOLCF/Domain.thy

     by (simp add: type_definition.Rep_inverse [OF type])
   have emb_prj: "\<And>y. emb\<cdot>(prj\<cdot>y :: 'a) = cast\<cdot>t\<cdot>y"
     unfolding prj_beta emb_beta
     by (simp add: type_definition.Abs_inverse [OF type])
   show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
-    apply default
+    apply standard
     apply (simp add: prj_emb)
     apply (simp add: emb_prj cast.below)
     done
   show "cast\<cdot>DEFL('a) = emb oo (prj :: udom \<rightarrow> 'a)"
     by (rule cfun_eqI, simp add: defl emb_prj)