diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -141,7 +141,7 @@
       {fix i assume i: "i \<in> ?U"
         from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
         have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
-          unfolding transpose_def by (simp add: expand_fun_eq)}
+          unfolding transpose_def by (simp add: ext_iff)}
       then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
     qed
     finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
@@ -207,7 +207,7 @@
   have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
   {fix p assume p: "p \<in> ?PU - {id}"
     then have "p \<noteq> id" by simp
-    then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto
+    then obtain i where i: "p i \<noteq> i" unfolding ext_iff by auto
     from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
     from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
   then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"  by blast