diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -53,11 +53,8 @@
 definition empty :: heap where
   "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
 
-datatype_new 'a array = Array addr -- "note the phantom type 'a"
-datatype_compat array
-
-datatype_new 'a ref = Ref addr -- "note the phantom type 'a"
-datatype_compat ref
+old_datatype 'a array = Array addr -- "note the phantom type 'a"
+old_datatype 'a ref = Ref addr -- "note the phantom type 'a"
 
 primrec addr_of_array :: "'a array \<Rightarrow> addr" where
   "addr_of_array (Array x) = x"