--- a/src/HOL/Rational.thy Sun Feb 15 16:25:39 2009 +0100
+++ b/src/HOL/Rational.thy Sun Feb 15 22:58:02 2009 +0100
@@ -801,7 +801,7 @@
then have "?c \<noteq> 0" by simp
then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
- by (simp add: semiring_div_class.mod_div_equality)
+ by (simp add: semiring_div_class.mod_div_equality)
moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
ultimately show ?thesis