# HG changeset patch
# User nipkow
# Date 1750951816 -7200
# Node ID 40e4e955c846e25e4f74bf4b70fb15fe2aac27ac
# Parent  8f866fd6fae1702670f0d0ed7b09e99bdac100aa
tuned

diff -r 8f866fd6fae1 -r 40e4e955c846 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 25 16:35:25 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 26 17:30:16 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)