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