src/HOL/SEQ.thy

--- a/src/HOL/SEQ.thy	Tue May 04 18:19:24 2010 +0200
+++ b/src/HOL/SEQ.thy	Tue May 04 20:26:53 2010 +0200
@@ -547,7 +547,7 @@
   assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
   shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
 proof (cases "finite A")
-  case True with assms show ?thesis
+  case True from this and assms show ?thesis
     by (induct A set: finite) (simp_all add: convergent_const convergent_add)
 qed (simp add: convergent_const)