diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jan 28 16:29:16 2009 +0100
@@ -240,7 +240,7 @@
     by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   then have "of_int x / of_int d = ?t / of_int d" 
     using cong[OF refl[of ?f] eq] by simp
-  then show ?thesis by (simp add: add_divide_distrib ring_simps prems)
+  then show ?thesis by (simp add: add_divide_distrib algebra_simps prems)
 qed
 
 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>