src/HOL/Nominal/Nominal.thy

 consts 
   perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
 
 (* a "private" copy of the option type used in the abstraction function *)
-datatype_new 'a noption = nSome 'a | nNone
+datatype 'a noption = nSome 'a | nNone
 
 datatype_compat noption
 
 (* a "private" copy of the product type used in the nominal induct method *)
-datatype_new ('a, 'b) nprod = nPair 'a 'b
+datatype ('a, 'b) nprod = nPair 'a 'b
 
 datatype_compat nprod
 
 (* an auxiliary constant for the decision procedure involving *) 
 (* permutations (to avoid loops when using perm-compositions)  *)