diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -189,13 +189,13 @@
 
 syntax
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
 syntax (xsymbols)
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 syntax (HTML output)
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}