avoid constructor name clash
authorblanchet
Wed, 21 Aug 2013 09:25:40 +0200
changeset 53123 00d922eba913
parent 53122 bc87b7af4767
child 53124 9ae9bbaccee1
avoid constructor name clash
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"