src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -1188,7 +1188,7 @@
   "card A > 0 \<Longrightarrow> finite A"
   by (rule ccontr) simp
 
-lemma card_0_eq [simp, no_atp]:
+lemma card_0_eq [simp]:
   "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
   by (auto dest: mk_disjoint_insert)