diff -r 5c9819d7713b -r a2874c8b3558 src/HOL/Cardinals/Fun_More_FP.thy
--- a/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy	Tue Nov 19 01:29:50 2013 +0100
@@ -232,7 +232,7 @@
 using assms
 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
       card_atLeastLessThan[of m] card_atLeastLessThan[of n]
-      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by auto
+      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce