# HG changeset patch
# User blanchet
# Date 1380034754 -7200
# Node ID 62c2f66ff9b2076f14d3a039dec2d5236537e83e
# Parent  92a8ae172242783b9c688590e15246a76c1fb509
use "primcorec" in example

diff -r 92a8ae172242 -r 62c2f66ff9b2 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]