src/HOL/Predicate.thy

 imports String
 begin
 
 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"
 
 lemma Pred_eval [simp]:

   by (rule ext, rule pred_eqI, auto)+
 
 
 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>"
 | "pred_of_seq (Insert x P) = single x \<squnion> P"
 | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"