1.1 --- a/src/HOLCF/Bifinite.thy	Sat Nov 27 12:55:12 2010 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Sat Nov 27 13:12:10 2010 -0800
     1.3 @@ -642,7 +642,7 @@
     1.4  apply (simp add: contlub_cfun_fun)
     1.5  apply (simp add: discr_approx_def)
     1.6  apply (case_tac x, simp)
     1.7 -apply (rule thelubI)
     1.8 +apply (rule lub_eqI)
     1.9  apply (rule is_lubI)
    1.10  apply (rule ub_rangeI, simp)
    1.11  apply (drule ub_rangeD)