--- a/src/HOL/Algebra/Module.thy Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/Module.thy Wed Nov 04 08:13:49 2015 +0100
@@ -14,7 +14,7 @@
record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
-locale module = R: cring + M: abelian_group M for M (structure) +
+locale module = R?: cring + M?: abelian_group M for M (structure) +
assumes smult_closed [simp, intro]:
"[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
and smult_l_distr: