--- a/src/HOL/BNF/Examples/Misc_Datatype.thy Wed Aug 21 22:40:55 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Datatype.thy Thu Aug 22 08:42:27 2013 +0200
@@ -56,6 +56,8 @@
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
+datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+
datatype_new ('a, 'b, 'c) some_killing =
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
and ('a, 'b, 'c) in_here =