diff -r de51a86fc903 -r cc97b347b301 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -252,7 +252,7 @@
   assume "q \<noteq> 0"
   then show "inverse q * q = 1"
     by (cases q rule: Fract_cases_nonzero)
-      (simp_all add: fract_expand eq_fract mult_commute)
+      (simp_all add: fract_expand eq_fract mult.commute)
 next
   fix q r :: "'a fract"
   show "q / r = q * inverse r" by (simp add: divide_fract_def)
@@ -398,7 +398,7 @@
     by (simp only: less_fract_def)
   show "q \<le> r \<or> r \<le> q"
     by (induct q, induct r)
-       (simp add: mult_commute, rule linorder_linear)
+       (simp add: mult.commute, rule linorder_linear)
 qed
 
 end