
diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 23 12:14:29 2010 +0100
@@ -149,7 +149,7 @@
 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
 
 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
-nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
+nitpick [card nat = 10, unary_ints, verbose, show_consts]
 oops
 
 lemma "even' (n - 2) \<Longrightarrow> even' n"




