--- 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 = [])"