# HG changeset patch
# User nipkow
# Date 1332788423 -7200
# Node ID af818dcdc709985fae017fe32ea477342833c103
# Parent  24a1cb3fdf09fd8213474c92764b751ed79334d3
reverted to canonical name

diff -r 24a1cb3fdf09 -r af818dcdc709 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 26 20:09:52 2012 +0200
+++ b/src/HOL/List.thy	Mon Mar 26 21:00:23 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 *}