--- a/src/HOLCF/FOCUS/Fstream.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Thu Jan 17 21:44:19 2008 +0100
@@ -239,7 +239,7 @@
apply (force)
apply (unfold max_in_chain_def)
apply auto
-apply (frule (1) chain_mono3)
+apply (frule (1) chain_mono)
apply (rule_tac x="Y j" in fstream_cases)
apply (force)
apply (drule_tac x="j" in is_ub_thelub)
@@ -254,7 +254,7 @@
apply (rule conjI)
apply (erule chain_shift [THEN chain_monofun])
apply safe
-apply (drule_tac x="j" and y="i+j" in chain_mono3)
+apply (drule_tac i="j" and j="i+j" in chain_mono)
apply (simp)
apply (simp)
apply (rule_tac x="i+j" in exI)