# HG changeset patch
# User nipkow
# Date 1750951833 -7200
# Node ID 59b937edcff8a7c10e00fb290863855b1b915d46
# Parent  4a1320dac3f34426ad4a1a069a60987ba5946f11# Parent  40e4e955c846e25e4f74bf4b70fb15fe2aac27ac
merged

diff -r 4a1320dac3f3 -r 59b937edcff8 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 26 17:16:14 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 26 17:30:33 2025 +0200
@@ -3417,7 +3417,7 @@
     "\<And>w x y z. f w x = f y z \<longleftrightarrow> w = y \<and> x = z" and
     "\<And>x y. f x y \<noteq> a" and
     "\<And>x y. f x y \<noteq> b"
-  shows "foldr f xs a = foldr f ys b \<longleftrightarrow> a = b \<and> xs = ys"
+  shows "foldr f xs a = foldr f ys b \<longleftrightarrow> xs = ys \<and> a = b"
 by (induction xs ys rule: list_induct2') (use assms(2,3,1) in auto)