diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-section {* Tree Implementation of Sets *}
+section \<open>Unbalanced Tree Implementation of Set\<close>
 
 theory Tree_Set
 imports
@@ -9,7 +9,7 @@
   Set_by_Ordered
 begin
 
-fun isin :: "'a::cmp tree \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node l a r) x =
   (case cmp x a of
@@ -19,7 +19,7 @@
 
 hide_const (open) insert
 
-fun insert :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "insert x Leaf = Node Leaf x Leaf" |
 "insert x (Node l a r) =
   (case cmp x a of
@@ -31,7 +31,7 @@
 "del_min (Node l a r) =
   (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
 
-fun delete :: "'a::cmp \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "delete x Leaf = Leaf" |
 "delete x (Node l a r) =
   (case cmp x a of