diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -2843,7 +2843,7 @@
     h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
   from h(2)
   have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
-    using sf by(auto simp add: surj_iff o_def fun_eq_iff)
+    using sf by(auto simp add: surj_iff_all)
   from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
   have "f o h = id" .
   then show ?thesis using h(1) by blast
@@ -2995,7 +2995,7 @@
   {fix f f':: "'a => 'a"
     assume lf: "linear f" "linear f'" and f: "f o f' = id"
     from f have sf: "surj f"
-      apply (auto simp add: o_def fun_eq_iff id_def surj_def)
+      apply (auto simp add: o_def id_def surj_def)
       by metis
     from linear_surjective_isomorphism[OF lf(1) sf] lf f
     have "f' o f = id" unfolding fun_eq_iff o_def id_def