# HG changeset patch
# User berghofe
# Date 1114102724 -7200
# Node ID 997884600e0a78889c1d812a10027ddf6a859769
# Parent  5de27a5fc5edbeffec24af3e91cd183f1998eb7a
Modified variable index in proof (necessary due to changes in the kernel).

diff -r 5de27a5fc5ed -r 997884600e0a src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Apr 21 18:57:18 2005 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Apr 21 18:58:44 2005 +0200
@@ -1058,7 +1058,7 @@
     apply (induct n)
     apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
     apply (auto)
-    by (drule_tac x1="(% j i. A j (Suc i))" in forall, simp)
+    by (drule_tac x3="(% j i. A j (Suc i))" in forall, simp)
   show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
     apply (simp add: foldmatrix_def foldmatrix_transposed_def)
     apply (induct m, simp)