diff -r 352c73a689da -r c3d6e570ccef src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Saturated.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -215,7 +215,7 @@
 end
 
 interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
-where
+rewrites
   "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
   show "semilattice_neutr_set min (top :: 'a sat)"
@@ -225,7 +225,7 @@
 qed
 
 interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
-where
+rewrites
   "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
   show "semilattice_neutr_set max (bot :: 'a sat)"