diff -r d5ff8b782b29 -r fee7cfa69c50 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Algebra/Module.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -118,7 +118,7 @@
 qed
 
 lemma (in algebra) smult_r_null [simp]:
-  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
+  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
 proof -
   assume R: "a \<in> carrier R"
   note facts = R smult_closed