diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Isin2.thy
--- a/src/HOL/Data_Structures/Isin2.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -9,7 +9,7 @@
   Set_by_Ordered
 begin
 
-fun isin :: "('a::cmp,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node _ l a r) x =
   (case cmp x a of