proper instantiation of mk_left_commute;

--- a/src/HOL/Library/Ring_and_Field.thy	Thu Aug 08 23:47:41 2002 +0200
+++ b/src/HOL/Library/Ring_and_Field.thy	Thu Aug 08 23:48:31 2002 +0200
@@ -90,7 +90,7 @@
 qed
 
 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
-by(rule mk_left_commute[OF mult_assoc mult_commute])
+  by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
 
 theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute