src/HOL/Data_Structures/Isin2.thy
changeset 68413 b56ed5010e69
parent 67967 5a4280946a25
child 70755 3fb16bed5d6c
     1.1 --- a/src/HOL/Data_Structures/Isin2.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
     1.6  "isin Leaf x = False" |
     1.7 -"isin (Node _ l a r) x =
     1.8 +"isin (Node l a _ r) x =
     1.9    (case cmp x a of
    1.10       LT \<Rightarrow> isin l x |
    1.11       EQ \<Rightarrow> True |