diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AA_Map.thy
--- a/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -8,7 +8,7 @@
   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
@@ -16,7 +16,7 @@
      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