src/HOL/Library/Fraction_Field.thy

 proof
   fix q :: "'a fract"
   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)
 next
   show "inverse 0 = (0:: 'a fract)"

     by (induct q) simp
   show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
     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
 
 instantiation fract :: (linordered_idom) "{distrib_lattice,abs_if,sgn_if}"