diff -r 1d43f86f48be -r e96292f32c3c src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -233,12 +233,12 @@
 
 end
 
-syntax
+syntax (ASCII)
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
-syntax (xsymbols)
+syntax
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
 translations
-  "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
+  "\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
 
 lemma Sum_any_left_distrib:
   fixes r :: "'a :: semiring_0"
@@ -302,10 +302,10 @@
 
 end
 
+syntax (ASCII)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
 syntax
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
-syntax (xsymbols)
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_. _)" [0, 10] 10)
 translations
   "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"