1.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    apply (simp)
     1.5    apply (force)
     1.6    apply (simp)
     1.7 -  apply (subst plus_ac0.commute[of m])
     1.8 +  apply (subst ab_semigroup_add.add_commute[of m])
     1.9    apply (simp)
    1.10    done
    1.11