--- a/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:56:52 2015 +0200
@@ -119,10 +119,10 @@
qed
instance "domain" \<subseteq> bifinite
-by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
+by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
instance predomain \<subseteq> profinite
-by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
+by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
subsection {* Universal domain ep-pairs *}