src/HOL/IMP/OO.thy

 abbreviation fun_upd2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
   ("_/'((2_,_ :=/ _)')" [1000,0,0,0] 900)
 where "f(x,y := z) == f(x := (f x)(y := z))"
 
 type_synonym addr = nat
-datatype ref = null | Ref addr
+datatype_new ref = null | Ref addr
 
 type_synonym obj = "string \<Rightarrow> ref"
 type_synonym venv = "string \<Rightarrow> ref"
 type_synonym store = "addr \<Rightarrow> obj"
 
-datatype exp =
+datatype_new exp =
   Null |
   New |
   V string |
   Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
   Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |