diff -r e1bd8a54c40f -r d7728f65b353 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOLCF/Algebraic.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -446,7 +446,7 @@
 apply (clarify, simp add: fd_take_fixed_iff)
 apply (simp add: finite_fixes_approx)
 apply (rule inj_onI, clarify)
-apply (simp add: set_ext_iff fin_defl_eqI)
+apply (simp add: set_eq_iff fin_defl_eqI)
 done
 
 lemma fd_take_covers: "\<exists>n. fd_take n a = a"