1.1 --- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:55:12 2010 -0800
     1.2 +++ b/src/HOLCF/Pcpodef.thy	Sat Nov 27 13:12:10 2010 -0800
     1.3 @@ -107,7 +107,7 @@
     1.4      by (rule typedef_is_lubI [OF below])
     1.5  qed
     1.6  
     1.7 -lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
     1.8 +lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard]
     1.9  
    1.10  theorem typedef_cpo:
    1.11    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"