src/HOLCF/Bifinite.thy

     by (rule finite_range_cfun_map)
   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
     by (rule finite_range_imp_finite_fixes)
 qed
 
-instantiation "->" :: (profinite, profinite) profinite
+instantiation cfun :: (profinite, profinite) profinite
 begin
 
 definition
   approx_cfun_def:
     "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"

               finite_deflation_approx)
 qed
 
 end
 
-instance "->" :: (profinite, bifinite) bifinite ..
+instance cfun :: (profinite, bifinite) bifinite ..
 
 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
 by (simp add: approx_cfun_def)
 
 end