diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- 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