src/HOL/HOLCF/FOCUS/Fstream.thy

--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 08:30:00 2010 -0800
@@ -250,7 +250,7 @@
 apply  (rule_tac x="i+j" in exI)
 apply  (drule fstream_prefix)
 apply  (clarsimp)
-apply  (subst contlub_cfun [symmetric])
+apply  (subst lub_APP)
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)