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