diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -271,7 +271,7 @@
     apply (intro strip)
     apply (frule_tac as=brr in sorted_spvec_cons1)
     apply (simp add: ring_eq_simps sparse_row_matrix_cons)
-    apply (subst Rep_matrix_zero_imp_mult_zero) 
+    apply (simplesubst Rep_matrix_zero_imp_mult_zero) 
     apply (simp)
     apply (intro strip)
     apply (rule disjI2)
@@ -805,9 +805,9 @@
   apply auto
   apply (case_tac "x=a")
   apply (simp)
-  apply (subst sorted_sparse_row_matrix_zero)
+  apply (simplesubst sorted_sparse_row_matrix_zero)
   apply auto
-  apply (subst Rep_sparse_row_vector_zero)
+  apply (simplesubst Rep_sparse_row_vector_zero)
   apply (simp_all add: neg_def)
   done