diff -r 9942c5ed866a -r 405fb812e738 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Mon Oct 10 05:30:02 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Mon Oct 10 05:46:17 2005 +0200
@@ -15,7 +15,7 @@
 
 subsection {* Definition of strict sum type *}
 
-pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
+pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
         "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
 by simp