--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:57 2014 +0100
@@ -746,17 +746,17 @@
nitpick [card = 1\<emdash>7, expect = none]
oops
-lemma "nat_rec zero suc 0 = zero"
+lemma "rec_nat zero suc 0 = zero"
nitpick [expect = none]
apply simp
done
-lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
+lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
nitpick [expect = none]
apply simp
done
-lemma "P (nat_rec zero suc x)"
+lemma "P (rec_nat zero suc x)"
nitpick [expect = genuine]
oops