--- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 23:46:45 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Apr 27 08:18:25 2010 +0200
@@ -55,7 +55,7 @@
done
(* FIXME: In Finite_Set there is a useless further assumption *)
-lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})"
+lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
apply (erule finite_induct)
apply (simp)
apply simp