src/HOL/BNF/Examples/ListF.thy

--- a/src/HOL/BNF/Examples/ListF.thy	Sat Aug 31 23:55:03 2013 +0200
+++ b/src/HOL/BNF/Examples/ListF.thy	Sun Sep 01 00:37:53 2013 +0200
@@ -12,7 +12,8 @@
 imports "../BNF"
 begin
 
-datatype_new 'a listF (map: mapF rel: relF) = NilF | Conss 'a "'a listF"
+datatype_new 'a listF (map: mapF rel: relF) =
+  NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
 datatype_new_compat listF
 
 definition Singll ("[[_]]") where