diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AA_Set.thy
--- a/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -1,5 +1,5 @@
 (*
-Author: Tobias Nipkow and Daniel Stüwe
+Author: Tobias Nipkow, Daniel Stüwe
 *)
 
 section \<open>AA Tree Implementation of Sets\<close>
@@ -36,7 +36,7 @@
 
 hide_const (open) insert
 
-fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
 "insert x Leaf = Node 1 Leaf x Leaf" |
 "insert x (Node lv t1 a t2) =
   (case cmp x a of
@@ -81,7 +81,7 @@
 "del_max (Node lv l a Leaf) = (l,a)" |
 "del_max (Node lv l a r) = (let (r',b) = del_max r in (adjust(Node lv l a r'), b))"
 
-fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
 "delete _ Leaf = Leaf" |
 "delete x (Node lv l a r) =
   (case cmp x a of