src/HOL/Data_Structures/Isin2.thy

--- a/src/HOL/Data_Structures/Isin2.thy	Mon Jun 11 08:15:43 2018 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy	Mon Jun 11 16:29:27 2018 +0200
@@ -11,7 +11,7 @@
 
 fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
-"isin (Node _ l a r) x =
+"isin (Node l a _ r) x =
   (case cmp x a of
      LT \<Rightarrow> isin l x |
      EQ \<Rightarrow> True |