Determinants.thy: avoid using mem_def/Collect_def

--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 17 14:42:59 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Aug 17 15:02:17 2011 -0700
@@ -131,7 +131,7 @@
   {fix p assume p: "p \<in> {p. p permutes ?U}"
     from p have pU: "p permutes ?U" by blast
     have sth: "sign (inv p) = sign p"
-      by (metis sign_inverse fU p mem_def Collect_def permutation_permutes)
+      by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
     from permutes_inj[OF pU]
     have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
     from permutes_image[OF pU]