src/HOL/Nitpick_Examples/Manual_Nits.thy

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 24 16:55:29 2013 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 24 16:59:14 2013 +0200
@@ -195,8 +195,8 @@
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
 
-primcorecursive iterates where
-"iterates f a = LCons a (iterates f (f a))" .
+primcorec iterates where
+"iterates f a = LCons a (iterates f (f a))"
 
 lemma "xs \<noteq> LCons a xs"
 nitpick [expect = genuine]