1.1 --- a/src/HOL/List.thy	Mon Mar 26 20:09:52 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Mar 26 21:00:23 2012 +0200
     1.3 @@ -5354,9 +5354,9 @@
     1.4    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
     1.5    by (simp add: list_all_iff)
     1.6  
     1.7 -lemma list_any_cong [fundef_cong]:
     1.8 +lemma list_ex_cong [fundef_cong]:
     1.9    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
    1.10 -  by (simp add: list_ex_iff)
    1.11 +by (simp add: list_ex_iff)
    1.12  
    1.13  text {* Executable checks for relations on sets *}
    1.14