src/HOLCF/UpperPD.thy

   "cast\<cdot>(upper_defl\<cdot>A) =
     udom_emb upper_approx oo upper_map\<cdot>(cast\<cdot>A) oo udom_prj upper_approx"
 using upper_approx finite_deflation_upper_map
 unfolding upper_defl_def by (rule cast_defl_fun1)
 
-instantiation upper_pd :: (bifinite) bifinite
+instantiation upper_pd :: (bifinite) liftdomain
 begin
 
 definition
   "emb = udom_emb upper_approx oo upper_map\<cdot>emb"
 

 definition
   "liftdefl (t::'a upper_pd itself) = u_defl\<cdot>DEFL('a upper_pd)"
 
 instance
 using liftemb_upper_pd_def liftprj_upper_pd_def liftdefl_upper_pd_def
-proof (rule bifinite_class_intro)
+proof (rule liftdomain_class_intro)
   show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)"
     unfolding emb_upper_pd_def prj_upper_pd_def
     using ep_pair_udom [OF upper_approx]
     by (intro ep_pair_comp ep_pair_upper_map ep_pair_emb_prj)
 next