# HG changeset patch
# User blanchet
# Date 1377069940 -7200
# Node ID 00d922eba9137ca2cfa3d9d9659a430ec788f0eb
# Parent  bc87b7af476740c98a31f1e80dd23a8c38bb6285
avoid constructor name clash

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"