src/HOL/IMP/OO.thy

--- a/src/HOL/IMP/OO.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/OO.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -8,13 +8,13 @@
 where "f(x,y := z) == f(x := (f x)(y := z))"
 
 type_synonym addr = nat
-datatype_new ref = null | Ref addr
+datatype ref = null | Ref addr
 
 type_synonym obj = "string \<Rightarrow> ref"
 type_synonym venv = "string \<Rightarrow> ref"
 type_synonym store = "addr \<Rightarrow> obj"
 
-datatype_new exp =
+datatype exp =
   Null |
   New |
   V string |