diff -r 8a02dd7fcb5d -r c833618d80eb src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 21 20:44:12 2025 +0200
+++ b/src/HOL/List.thy	Thu May 22 19:59:43 2025 +0200
@@ -3769,6 +3769,9 @@
   case False with d show ?thesis by auto
 qed
 
+lemma distinct_concat_rev[simp]: "distinct (concat (rev xs)) = distinct (concat xs)"
+by (induction xs) auto
+
 lemma distinct_concat:
   "\<lbrakk> distinct xs;
      \<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys;
@@ -4285,6 +4288,7 @@
   qed
 qed
 
+
 subsection \<open>@{const distinct_adj}\<close>
 
 lemma distinct_adj_Nil [simp]: "distinct_adj []"