src/HOL/HOLCF/Bifinite.thy

--- a/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -253,7 +253,7 @@
 qed
 
 lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
-by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
+by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
 
 instance unit :: bifinite
   by default (fast intro!: approx_chain_unit)