src/HOL/Library/Extended_Nat.thy

--- a/src/HOL/Library/Extended_Nat.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -487,7 +487,7 @@
 proof (rule finite_subset)
   show "finite (enat ` {..n})" by blast
 
-  have "A \<subseteq> {..enat n}" using le_fin by fastsimp
+  have "A \<subseteq> {..enat n}" using le_fin by fastforce
   also have "\<dots> \<subseteq> enat ` {..n}"
     by (rule subsetI) (case_tac x, auto)
   finally show "A \<subseteq> enat ` {..n}" .