diff -r 7fa91e6176ed -r 13f3768a6f14 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Jul 13 20:53:26 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Thu Jul 14 01:04:30 2005 +0200
@@ -206,13 +206,9 @@
 apply (rule contI)
 apply (drule ssum_chain_lemma, safe)
 apply (simp add: contlub_cfun_arg [symmetric])
-apply (simp add: Iwhen4)
-apply (simp add: contlub_cfun_arg)
-apply (simp add: thelubE chain_monofun)
+apply (simp add: Iwhen4 cont_cfun_arg)
 apply (simp add: contlub_cfun_arg [symmetric])
-apply (simp add: Iwhen5)
-apply (simp add: contlub_cfun_arg)
-apply (simp add: thelubE chain_monofun)
+apply (simp add: Iwhen5 cont_cfun_arg)
 done
 
 subsection {* Continuous versions of constants *}