--- a/src/HOL/List.thy Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/List.thy Mon Nov 17 17:00:55 2008 +0100
@@ -549,9 +549,9 @@
by (induct xs) auto
interpretation semigroup_append: semigroup_add ["op @"]
-by unfold_locales simp
+ proof qed simp
interpretation monoid_append: monoid_add ["[]" "op @"]
-by unfold_locales (simp+)
+ proof qed simp+
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
by (induct xs) auto
@@ -3834,7 +3834,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma lenght_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code inline]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all