diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Lattices.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -271,7 +271,7 @@
 context semilattice_inf
 begin
 
-sublocale inf!: semilattice inf
+sublocale inf: semilattice inf
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -282,7 +282,7 @@
     by (rule antisym) (auto simp add: le_inf_iff)
 qed
 
-sublocale inf!: semilattice_order inf less_eq less
+sublocale inf: semilattice_order inf less_eq less
   by standard (auto simp add: le_iff_inf less_le)
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
@@ -316,7 +316,7 @@
 context semilattice_sup
 begin
 
-sublocale sup!: semilattice sup
+sublocale sup: semilattice sup
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
@@ -327,7 +327,7 @@
     by (rule antisym) (auto simp add: le_sup_iff)
 qed
 
-sublocale sup!: semilattice_order sup greater_eq greater
+sublocale sup: semilattice_order sup greater_eq greater
   by standard (auto simp add: le_iff_sup sup.commute less_le)
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
@@ -484,8 +484,8 @@
 class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
 
-sublocale inf_top!: semilattice_neutr inf top
-  + inf_top!: semilattice_neutr_order inf top less_eq less
+sublocale inf_top: semilattice_neutr inf top
+  + inf_top: semilattice_neutr_order inf top less_eq less
 proof
   fix x
   show "x \<sqinter> \<top> = x"
@@ -497,8 +497,8 @@
 class bounded_semilattice_sup_bot = semilattice_sup + order_bot
 begin
 
-sublocale sup_bot!: semilattice_neutr sup bot
-  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
+sublocale sup_bot: semilattice_neutr sup bot
+  + sup_bot: semilattice_neutr_order sup bot greater_eq greater
 proof
   fix x
   show "x \<squnion> \<bottom> = x"
@@ -715,8 +715,8 @@
 context linorder
 begin
 
-sublocale min!: semilattice_order min less_eq less
-  + max!: semilattice_order max greater_eq greater
+sublocale min: semilattice_order min less_eq less
+  + max: semilattice_order max greater_eq greater
   by standard (auto simp add: min_def max_def)
 
 lemma min_le_iff_disj: