--- a/src/HOL/HOLCF/Ssum.thy Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Ssum.thy Tue Oct 09 17:33:46 2012 +0200
@@ -19,7 +19,7 @@
(fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
(fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
-pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
unfolding ssum_def by simp_all
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin