--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -122,7 +122,7 @@
subsection {* Trees *}
-datatype_new 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
+datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
primrec leaves :: "'a tree \<Rightarrow> 'a list" where
"leaves Twig = []"
@@ -150,7 +150,7 @@
--{* Wrong! *}
oops
-datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
+datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
"inOrder (Tip a)= [a]"
@@ -439,7 +439,7 @@
quickcheck[random, expect = counterexample]
oops
-datatype_new colour = Red | Green | Blue
+datatype colour = Red | Green | Blue
record cpoint = point +
colour :: colour