# HG changeset patch
# User blanchet
# Date 1410624525 -7200
# Node ID ec949d7206bbc6b411626b4bf0a2cda0e3ff2637
# Parent  be0f5d8d511bd043e9a5544bdbe3892e699e91a7
ported Imperative HOL to new datatypes

diff -r be0f5d8d511b -r ec949d7206bb src/HOL/Imperative_HOL/Heap.thy
--- 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"
diff -r be0f5d8d511b -r ec949d7206bb src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- 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"