--- a/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Oct 23 09:58:30 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Oct 23 14:53:36 2013 +0200
@@ -19,7 +19,7 @@
 
 datatype_new simple'' = X1'' nat int | X2''
 
-datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
+datatype_new 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
 
 datatype_new ('b, 'c, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e