1.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 12:55:12 2010 -0800
     1.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Sat Nov 27 13:12:10 2010 -0800
     1.3 @@ -37,7 +37,7 @@
     1.4  prefer 2 apply fast
     1.5  apply (unfold finite_chain_def)
     1.6  apply safe
     1.7 -apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
     1.8 +apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
     1.9  apply assumption
    1.10  apply (erule spec)
    1.11  done