1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4        apply simp
     1.5        apply algebra
     1.6        done
     1.7 -    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
     1.8 +    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
     1.9        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
    1.10        have eq1: "b = b'" using pos by arith  
    1.11        with eq have "a = a'" using pos by simp