diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 03 00:06:24 2014 +0200
@@ -10,7 +10,7 @@
 
 subsection {* The type of predicate enumerations (a monad) *}
 
-datatype 'a pred = Pred "'a \<Rightarrow> bool"
+datatype_new '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 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
+datatype_new '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>"