src/HOL/Library/Abstract_Rat.thy

--- a/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 09:58:45 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 20:52:30 2009 +0100
@@ -247,7 +247,7 @@
     (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
   apply (frule of_int_div_aux [of d n, where ?'a = 'a])
   apply simp
-  apply (simp add: zdvd_iff_zmod_eq_0)
+  apply (simp add: dvd_eq_mod_eq_0)
 done