# HG changeset patch
# User nipkow
# Date 1332788439 -7200
# Node ID bef6bc52a32e5d3268639fb8996774b2d5077a37
# Parent  bd1679890503fa1a119079b2f0dd30444b3a19aa# Parent  af818dcdc709985fae017fe32ea477342833c103
merged

diff -r bd1679890503 -r bef6bc52a32e src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 26 20:11:27 2012 +0200
+++ b/src/HOL/List.thy	Mon Mar 26 21:00:39 2012 +0200
@@ -5354,9 +5354,9 @@
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
   by (simp add: list_all_iff)
 
-lemma list_any_cong [fundef_cong]:
+lemma list_ex_cong [fundef_cong]:
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
-  by (simp add: list_ex_iff)
+by (simp add: list_ex_iff)
 
 text {* Executable checks for relations on sets *}