src/HOL/HOLCF/Bifinite.thy

     using bifinite [where 'a='a]
     by (fast intro!: approx_chain_u_map)
 qed
 
 instance u :: (profinite) bifinite
-  by default (rule profinite)
+  by standard (rule profinite)
 
 text {*
   Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
 *}
 

 
 lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
 by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
 
 instance unit :: bifinite
-  by default (fast intro!: approx_chain_unit)
+  by standard (fast intro!: approx_chain_unit)
 
 instance discr :: (countable) profinite
-  by default (fast intro!: discr_approx)
+  by standard (fast intro!: discr_approx)
 
 instance lift :: (countable) bifinite
 proof
   note [simp] = cont_Abs_lift cont_Rep_lift Rep_lift_inverse Abs_lift_inverse
   obtain a :: "nat \<Rightarrow> ('a discr)\<^sub>\<bottom> \<rightarrow> ('a discr)\<^sub>\<bottom>" where a: "approx_chain a"