tuned

--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:07 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 08:56:08 2014 +0100
@@ -711,7 +711,7 @@
 
 corollary card_of_Sigma_Times:
 "\<forall>i \<in> I. |A i| \<le>o |B| \<Longrightarrow> |SIGMA i : I. A i| \<le>o |I \<times> B|"
-using card_of_Sigma_mono1[of I A "\<lambda>i. B"] .
+by (fact card_of_Sigma_mono1)
 
 lemma card_of_UNION_Sigma:
 "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"