diff -r 4d7e3cc9c52c -r 059d2f7b979f src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Mar 11 14:39:58 2010 +0100
+++ b/src/HOL/Rat.thy	Thu Mar 11 14:39:58 2010 +0100
@@ -1104,11 +1104,11 @@
 
 lemma rat_less_eq_code [code]:
   "p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)"
-  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
+  by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
 
 lemma rat_less_code [code]:
   "p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)"
-  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
+  by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
 
 lemma [code]:
   "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"