1.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 12:55:12 2010 -0800
     1.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Sat Nov 27 13:12:10 2010 -0800
     1.3 @@ -246,7 +246,7 @@
     1.4  apply (drule fstreams_lub_lemma1, auto)
     1.5  apply (rule_tac x="j" in exI, auto)
     1.6  apply (case_tac "max_in_chain j Y")
     1.7 -apply (frule lub_finch1 [THEN thelubI], auto)
     1.8 +apply (frule lub_finch1 [THEN lub_eqI], auto)
     1.9  apply (rule_tac x="j" in exI)
    1.10  apply (erule subst) back back
    1.11  apply (simp add: below_prod_def sconc_mono)
    1.12 @@ -266,7 +266,7 @@
    1.13  lemma lub_Pair_not_UU_lemma: 
    1.14    "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
    1.15        ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
    1.16 -apply (frule thelub_cprod, clarsimp)
    1.17 +apply (frule lub_prod, clarsimp)
    1.18  apply (drule chain_UU_I_inverse2, clarsimp)
    1.19  apply (case_tac "Y i", clarsimp)
    1.20  apply (case_tac "max_in_chain i Y")
    1.21 @@ -298,7 +298,7 @@
    1.22  apply (drule fstreams_lub_lemma2, auto)
    1.23  apply (rule_tac x="j" in exI, auto)
    1.24  apply (case_tac "max_in_chain j Y")
    1.25 -apply (frule lub_finch1 [THEN thelubI], auto)
    1.26 +apply (frule lub_finch1 [THEN lub_eqI], auto)
    1.27  apply (rule_tac x="j" in exI)
    1.28  apply (erule subst) back back
    1.29  apply (simp add: sconc_mono)
    1.30 @@ -312,7 +312,7 @@
    1.31  apply (rule sconc_mono)
    1.32  apply (subgoal_tac "tt ~= tta" "tta << ms")
    1.33  apply (blast intro: fstreams_chain_lemma)
    1.34 -apply (frule lub_cprod [THEN thelubI], auto)
    1.35 +apply (frule lub_prod, auto)
    1.36  apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
    1.37  apply (drule fstreams_mono, simp)
    1.38  apply (rule is_ub_thelub chainI)