diff -r ba7901e94e7b -r aa03b0487bf5 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Jul 11 10:43:27 2016 +0200
@@ -215,10 +215,8 @@
 begin
 
 sublocale Sum_any: comm_monoid_fun plus 0
-defines
-  Sum_any = Sum_any.G
-rewrites
-  "comm_monoid_set.F plus 0 = setsum"
+  defines Sum_any = Sum_any.G
+  rewrites "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_fun plus 0" ..
   then interpret Sum_any: comm_monoid_fun plus 0 .
@@ -284,10 +282,8 @@
 begin
 
 sublocale Prod_any: comm_monoid_fun times 1
-defines
-  Prod_any = Prod_any.G
-rewrites
-  "comm_monoid_set.F times 1 = setprod"
+  defines Prod_any = Prod_any.G
+  rewrites "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_fun times 1" ..
   then interpret Prod_any: comm_monoid_fun times 1 .