diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Complex.thy Mon Apr 26 15:37:50 2010 +0200 @@ -99,7 +99,7 @@ subsection {* Multiplication and Division *} -instantiation complex :: "{field, division_ring_inverse_zero}" +instantiation complex :: field_inverse_zero begin definition