diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/Lookup2.thy
--- a/src/HOL/Data_Structures/Lookup2.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/Lookup2.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -9,7 +9,7 @@
   Map_by_Ordered
 begin
 
-fun lookup :: "('a::cmp * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
 "lookup Leaf x = None" |
 "lookup (Node _ l (a,b) r) x =
   (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"