diff -r 7a6c17b826c0 -r d1641dba61e5 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Jul 07 18:25:02 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Thu Jul 07 18:38:00 2005 +0200
@@ -148,7 +148,7 @@
   apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI)
   apply (rule conjI)
    apply (rule chain_monofun)
-   apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+   apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
   apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
   apply (drule less_sinlD, clarify)
   apply (simp add: sinl_eq Rep_Ssum_sinl)
@@ -156,7 +156,7 @@
  apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
  apply (rule conjI)
   apply (rule chain_monofun)
-  apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+  apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
  apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
  apply (drule less_sinrD, clarify)
  apply (simp add: sinr_eq Rep_Ssum_sinr)