diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
 
 subsection {* The type of predicate enumerations (a monad) *}
 
-datatype_new 'a pred = Pred "'a \<Rightarrow> bool"
+datatype 'a pred = Pred "'a \<Rightarrow> bool"
 
 primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
   eval_pred: "eval (Pred f) = f"
@@ -402,7 +402,7 @@
 
 subsection {* Implementation *}
 
-datatype_new 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
+datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
 
 primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
   "pred_of_seq Empty = \<bottom>"