
diff -r bc87b7af4767 -r 00d922eba913 src/HOL/BNF/Examples/Misc_Datatype.thy
--- a/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Aug 21 09:25:40 2013 +0200
@@ -154,7 +154,7 @@
 datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
 datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
 datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
-datatype_new 'a deadfoo = C "'a \<Rightarrow> 'a + 'a"
+datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
 
 datatype_new 'a dead_foo = A
 datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"




