src/HOL/Data_Structures/AA_Map.thy

 imports
   AA_Set
   Lookup2
 begin
 
-fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
 "update x y Leaf = Node 1 Leaf (x,y) Leaf" |
 "update x y (Node lv t1 (a,b) t2) =
   (case cmp x a of
      LT \<Rightarrow> split (skew (Node lv (update x y t1) (a,b) t2)) |
      GT \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) |
      EQ \<Rightarrow> Node lv t1 (x,y) t2)"
 
-fun delete :: "'a::cmp \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
 "delete _ Leaf = Leaf" |
 "delete x (Node lv l (a,b) r) =
   (case cmp x a of
      LT \<Rightarrow> adjust (Node lv (delete x l) (a,b) r) |
      GT \<Rightarrow> adjust (Node lv l (a,b) (delete x r)) |