diff -r cc1d4c3ca9db -r ae634fad947e src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Jan 28 11:48:43 2010 +0100
@@ -1200,14 +1200,18 @@
     by (rule poly_dvd_antisym)
 qed
 
-lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
-by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+interpretation poly_gcd!: abel_semigroup poly_gcd
+proof
+  fix x y z :: "'a poly"
+  show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+    by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+  show "poly_gcd x y = poly_gcd y x"
+    by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+qed
 
-lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
-by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
-
-lemmas poly_gcd_left_commute =
-  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+lemmas poly_gcd_assoc = poly_gcd.assoc
+lemmas poly_gcd_commute = poly_gcd.commute
+lemmas poly_gcd_left_commute = poly_gcd.left_commute
 
 lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute