# HG changeset patch
# User nipkow
# Date 1548923415 -3600
# Node ID d10fafeb93c0c08e12eee6b08183a430393a8e74
# Parent  76fbd806ebc534d416667e1af062c438c87b81bb
less special syntax: make \<Sum> an ordinary function symbol

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