# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 0662f35534fe69aba8b3f0c8848a35d2d81d38fc
# Parent  08c0f0d4b9f4483d675ad932376ab7c06e121182
half-ported Imperative HOL to new datatypes

diff -r 08c0f0d4b9f4 -r 0662f35534fe src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -53,8 +53,11 @@
 definition empty :: heap where
   "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
 
-datatype_new 'a array = Array addr
-datatype_new 'a ref = Ref addr -- "note the phantom type 'a "
+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
 
 primrec addr_of_array :: "'a array \<Rightarrow> addr" where
   "addr_of_array (Array x) = x"
diff -r 08c0f0d4b9f4 -r 0662f35534fe src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 20:51:36 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"}) *}
-datatype_new '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"
diff -r 08c0f0d4b9f4 -r 0662f35534fe src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -1056,7 +1056,7 @@
 theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = map_option (f x) (rbt_lookup t x)"
   apply(induct t)
   apply auto
-  apply(subgoal_tac "x = a")
+  apply(rename_tac a b c, subgoal_tac "x = a")
   apply auto
   done
  (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
@@ -1749,7 +1749,7 @@
 hide_type (open) compare
 hide_const (open)
   compare_height skip_black skip_red LT GT EQ case_compare rec_compare
-  Abs_compare Rep_compare rep_set_compare
+  Abs_compare Rep_compare
 hide_fact (open)
   Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
   Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse