diff -r 0acff85f95c7 -r f7d8cfa6e7fc src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:43:52 2010 -0800
+++ b/src/HOL/HOLCF/Fixrec.thy	Mon Dec 06 08:59:58 2010 -0800
@@ -36,10 +36,10 @@
 done
 
 lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>"
-by (simp add: succeed_def cont_Abs_match Abs_match_defined)
+by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)
 
 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
-by (simp add: fail_def Abs_match_defined)
+by (simp add: fail_def Abs_match_bottom_iff)
 
 lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)"
 by (simp add: succeed_def cont_Abs_match Abs_match_inject)