diff -r 40abbc7c86df -r e98f59806244 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -132,14 +132,14 @@
 apply (rule exI[of _ n], simp add: split_if)+
 by (simp add: split_if)
 
-lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
 proof -
   have "?r <= n" by (simp add: nrows_le)
   moreover have "n <= ?r" by (simp add:le_nrows, arith)
   ultimately show "?r = n" by simp
 qed
 
-lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
 proof -
   have "?r <= n" by (simp add: ncols_le)
   moreover have "n <= ?r" by (simp add: le_ncols, arith)