--- a/RedBlackTree.agda	Thu Jan 11 15:16:44 2018 +0900
+++ b/RedBlackTree.agda	Thu Jan 11 17:38:13 2018 +0900
@@ -198,15 +198,14 @@
 getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
 getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
   where
+    search : Node a k -> t
     checkNode : Maybe (Node a k) -> t
     checkNode Nothing = cs tree Nothing
     checkNode (Just n) = search n
-      where
-        search : Node a k -> t
-        search n with compare tree (key n) k1
-        search n | LT = checkNode (left n)
-        search n | GT = checkNode (right n)
-        search n | EQ = cs tree (Just n)
+    search n with compare tree k1 (key n) 
+    search n | LT = checkNode (left n)
+    search n | GT = checkNode (right n)
+    search n | EQ = cs tree (Just n)
 
 open import Data.Nat hiding (compare)