--- a/src/HOL/Data_Structures/Lookup2.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Data_Structures/Lookup2.thy Thu Jul 07 18:08:02 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)"