--- a/src/HOL/Algebra/AbelCoset.thy Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Nov 04 08:13:49 2015 +0100
@@ -51,7 +51,7 @@
kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
-locale abelian_group_hom = G: abelian_group G + H: abelian_group H
+locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
for G (structure) and H (structure) +
fixes h
assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>