diff -r f4b1cf9e7010 -r 0f8cb5568b63 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat Mar 03 22:33:25 2018 +0100
+++ b/src/HOL/Library/FSet.thy	Sun Mar 04 12:22:48 2018 +0100
@@ -751,8 +751,8 @@
 context comm_monoid_add begin
 
 sublocale fsum: comm_monoid_fset plus 0
+  rewrites "comm_monoid_set.F plus 0 = sum"
   defines fsum = fsum.F
-  rewrites "comm_monoid_set.F plus 0 = sum"
 proof -
   show "comm_monoid_fset (+) 0" by standard
 
@@ -797,8 +797,8 @@
 context linorder begin
 
 sublocale fMin: semilattice_order_fset min less_eq less
+  rewrites "semilattice_set.F min = Min"
   defines fMin = fMin.F
-  rewrites "semilattice_set.F min = Min"
 proof -
   show "semilattice_order_fset min (\<le>) (<)" by standard
 
@@ -806,8 +806,8 @@
 qed
 
 sublocale fMax: semilattice_order_fset max greater_eq greater
+  rewrites "semilattice_set.F max = Max"
   defines fMax = fMax.F
-  rewrites "semilattice_set.F max = Max"
 proof -
   show "semilattice_order_fset max (\<ge>) (>)"
     by standard