1.1 --- a/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -802,7 +802,7 @@
     1.4    then have "?c \<noteq> 0" by simp
     1.5    then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
     1.6    moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
     1.7 -   by (simp add: times_div_mod_plus_zero_one.mod_div_equality)
     1.8 +   by (simp add: semiring_div_class.mod_div_equality)
     1.9    moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.10    moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.11    ultimately show ?thesis