--- a/src/HOL/List.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/List.thy Mon Sep 13 11:13:15 2010 +0200
@@ -2317,7 +2317,7 @@
lemma foldl_apply:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
- by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: ext_iff)
+ by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
lemma foldl_cong [fundef_cong, recdef_cong]:
"[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
@@ -4564,7 +4564,7 @@
lemma member_set:
"member = set"
- by (simp add: ext_iff member_def mem_def)
+ by (simp add: fun_eq_iff member_def mem_def)
lemma member_rec [code]:
"member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"