--- 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>"