# HG changeset patch
# User wenzelm
# Date 1028843311 -7200
# Node ID 0e6adce08fb0346b938f3186d4d8eaf97114ca06
# Parent  2bb7200a99cf70a6c41cd45ee8341e4fe905cb5e
proper instantiation of mk_left_commute;

diff -r 2bb7200a99cf -r 0e6adce08fb0 src/HOL/Library/Ring_and_Field.thy
--- 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