diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Groups_List.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -65,12 +65,12 @@
 where
   "listsum  = monoid_list.F plus 0"
 
-sublocale listsum!: monoid_list plus 0
+sublocale listsum: monoid_list plus 0
 rewrites
  "monoid_list.F plus 0 = listsum"
 proof -
   show "monoid_list plus 0" ..
-  then interpret listsum!: monoid_list plus 0 .
+  then interpret listsum: monoid_list plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
 qed
  
@@ -79,22 +79,22 @@
 context comm_monoid_add
 begin
 
-sublocale listsum!: comm_monoid_list plus 0
+sublocale listsum: comm_monoid_list plus 0
 rewrites
   "monoid_list.F plus 0 = listsum"
 proof -
   show "comm_monoid_list plus 0" ..
-  then interpret listsum!: comm_monoid_list plus 0 .
+  then interpret listsum: comm_monoid_list plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
 qed
 
-sublocale setsum!: comm_monoid_list_set plus 0
+sublocale setsum: comm_monoid_list_set plus 0
 rewrites
   "monoid_list.F plus 0 = listsum"
   and "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_list_set plus 0" ..
-  then interpret setsum!: comm_monoid_list_set plus 0 .
+  then interpret setsum: comm_monoid_list_set plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
 qed
@@ -332,12 +332,12 @@
 where
   "listprod  = monoid_list.F times 1"
 
-sublocale listprod!: monoid_list times 1
+sublocale listprod: monoid_list times 1
 rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "monoid_list times 1" ..
-  then interpret listprod!: monoid_list times 1 .
+  then interpret listprod: monoid_list times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
 qed
 
@@ -346,22 +346,22 @@
 context comm_monoid_mult
 begin
 
-sublocale listprod!: comm_monoid_list times 1
+sublocale listprod: comm_monoid_list times 1
 rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "comm_monoid_list times 1" ..
-  then interpret listprod!: comm_monoid_list times 1 .
+  then interpret listprod: comm_monoid_list times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
 qed
 
-sublocale setprod!: comm_monoid_list_set times 1
+sublocale setprod: comm_monoid_list_set times 1
 rewrites
   "monoid_list.F times 1 = listprod"
   and "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_list_set times 1" ..
-  then interpret setprod!: comm_monoid_list_set times 1 .
+  then interpret setprod: comm_monoid_list_set times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
 qed