--- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
 
 text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
 
-datatype_new 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
+datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
 
 fun "fun" where "fun (FunDom f xs) = f"
 fun dom where "dom (FunDom f xs) = xs"