--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 14:11:02 2011 -0700
@@ -533,7 +533,7 @@
case False hence "t = {}" using `finite t` by auto
show ?thesis
proof (cases "s = {}")
- have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by (auto intro: ext)
+ have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
case True thus ?thesis using `t = {}` by (auto simp: *)
next
case False thus ?thesis using `t = {}` by simp