--- 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"