--- a/src/HOL/Imperative_HOL/Heap.thy Sat Sep 13 18:08:38 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Sat Sep 13 18:08:45 2014 +0200
@@ -53,8 +53,8 @@
definition empty :: heap where
"empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
-old_datatype 'a array = Array addr -- "note the phantom type 'a"
-old_datatype 'a ref = Ref addr -- "note the phantom type 'a"
+datatype 'a array = Array addr -- "note the phantom type 'a"
+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"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sat Sep 13 18:08:38 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sat Sep 13 18:08:45 2014 +0200
@@ -11,7 +11,7 @@
section {* Definition of Linked Lists *}
setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
-old_datatype 'a node = Empty | Node 'a "'a node ref"
+datatype 'a node = Empty | Node 'a "'a node ref"
primrec
node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"