--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 11:05:32 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 12:14:29 2010 +0100
@@ -143,11 +143,11 @@
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Zero_nat_def_raw)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Suc_def)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"