src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -1620,8 +1620,7 @@
   show False by simp (blast dest: Suc_neq_Zero surjD)
 qed
 
-(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
-lemma infinite_UNIV_char_0 [no_atp]:
+lemma infinite_UNIV_char_0:
   "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
 proof
   assume "finite (UNIV :: 'a set)"