diff -r b7148ee355f6 -r 5bd33fa698c7 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 07 22:07:52 2025 +0200
+++ b/src/HOL/List.thy	Fri May 09 14:15:10 2025 +0200
@@ -1330,11 +1330,16 @@
 
 lemmas set_empty2[iff] = set_empty[THEN eq_iff_swap]
 
+lemma append_eq_append_conv_if_disj:
+  "(set xs \<union> set xs') \<inter> (set ys \<union> set ys') = {}
+  \<Longrightarrow>  xs @ ys = xs' @ ys' \<longleftrightarrow> xs = xs' \<and> ys = ys'"
+by (auto simp: all_conj_distrib disjoint_iff append_eq_append_conv2)
+
 lemma set_rev [simp]: "set (rev xs) = set xs"
 by (induct xs) auto
 
 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
-by (induct xs) auto
+by (rule list.set_map)
 
 lemma set_filter [simp]: "set (filter P xs) = {x. x \<in> set xs \<and> P x}"
 by (induct xs) auto