diff --git a/tests/lean/run/matchWithSearch.lean b/tests/lean/run/matchWithSearch.lean
index c13b35f7b3..970ec886ea 100644
--- a/tests/lean/run/matchWithSearch.lean
+++ b/tests/lean/run/matchWithSearch.lean
@@ -26,21 +26,21 @@ inductive almostNode : Nat → Type
   | V {h c} (node:rbnode h c) : almostNode h
 open almostNode
 
-def balanceRR {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
+def balanceRR (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
   match h, c, left, right with
   | _, _, left, HR c => RR left y c
   | _, _, R a x b, HB c => LR (R a x b) y c
   | _, _, B a x b, HB c => V (R (B a x b) y c)
   | _, _, Leaf, HB c => V (R Leaf y c)
 
-def balanceRR' {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
+def balanceRR' (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
   match h, c, right, left with
   | _, _, HR c, left => RR left y c
   | _, _, HB c, R a x b => LR (R a x b) y c
   | _, _, HB c, B a x b => V (R (B a x b) y c)
   | _, _, HB c, Leaf => V (R Leaf y c)
 
-def balanceRR'' {h c} (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
+def balanceRR'' (left : rbnode h c) (y : Int) (right : hiddenTree h) : almostNode h :=
   match left, right with
   | left,    HR c => RR left y c
   | R a x b, HB c => LR (R a x b) y c