--- a/src/HOL/List.thy Wed Dec 10 17:19:25 2008 +0100
+++ b/src/HOL/List.thy Thu Dec 11 18:30:26 2008 +0100
@@ -548,9 +548,9 @@
lemma append_Nil2 [simp]: "xs @ [] = xs"
by (induct xs) auto
-interpretation semigroup_append: semigroup_add ["op @"]
+class_interpretation semigroup_append: semigroup_add ["op @"]
proof qed simp
-interpretation monoid_append: monoid_add ["[]" "op @"]
+class_interpretation monoid_append: monoid_add ["[]" "op @"]
proof qed simp+
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"