diff -r 76fbd806ebc5 -r d10fafeb93c0 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Jan 30 22:46:49 2019 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Jan 31 09:30:15 2019 +0100
@@ -534,8 +534,8 @@
 sublocale sum: comm_monoid_set plus 0
   defines sum = sum.F ..
 
-abbreviation Sum ("\<Sum>_" [1000] 999)
-  where "\<Sum>A \<equiv> sum (\<lambda>x. x) A"
+abbreviation Sum ("\<Sum>")
+  where "\<Sum> \<equiv> sum (\<lambda>x. x)"
 
 end