diff -r 1aa23e9f2c87 -r 138f414f14cb src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jan 04 15:32:56 2011 -0800
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jan 04 15:46:38 2011 -0800
@@ -233,7 +233,7 @@
 
 lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
 apply (subgoal_tac "(LUB i. Y i) ~= UU")
-apply (drule chain_UU_I_inverse2, auto)
+apply (frule lub_eq_bottom_iff, auto)
 apply (drule_tac x="i" in is_ub_thelub, auto)
 by (drule fstreams_prefix' [THEN iffD1], auto)
 
@@ -267,7 +267,7 @@
   "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
       ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
 apply (frule lub_prod, clarsimp)
-apply (drule chain_UU_I_inverse2, clarsimp)
+apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"])
 apply (case_tac "Y i", clarsimp)
 apply (case_tac "max_in_chain i Y")
 apply (drule maxinch_is_thelub, auto)