src/HOLCF/Algebraic.thy

 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"])
 apply (rule finite_subset [where B="Pow {x. approx n\<cdot>x = x}"])
 apply (clarify, simp add: fd_take_fixed_iff)
 apply (simp add: finite_fixes_approx)
 apply (rule inj_onI, clarify)
-apply (simp add: expand_set_eq fin_defl_eqI)
+apply (simp add: set_ext_iff fin_defl_eqI)
 done
 
 lemma fd_take_covers: "\<exists>n. fd_take n a = a"
 apply (rule_tac x=
   "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)