diff -r 555e5358b8c9 -r a4179bf442d1 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:14:04 2009 +0100
@@ -206,7 +206,7 @@
       apply simp
       apply algebra
       done
-    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
+    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
       coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
       have eq1: "b = b'" using pos by arith  
       with eq have "a = a'" using pos by simp