diff -r c6d2d23909d1 -r 1ff0f3f08a7b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/List.thy	Fri Jan 16 14:58:11 2009 +0100
@@ -547,9 +547,9 @@
 lemma append_Nil2 [simp]: "xs @ [] = xs"
 by (induct xs) auto
 
-class_interpretation semigroup_append: semigroup_add ["op @"]
+interpretation semigroup_append!: semigroup_add "op @"
   proof qed simp
-class_interpretation monoid_append: monoid_add ["[]" "op @"]
+interpretation monoid_append!: monoid_add "[]" "op @"
   proof qed simp+
 
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"