diff --git a/tests/lean/run/dep_subst.lean b/tests/lean/run/dep_subst.lean
index 3e14134e5..bbba1bff4 100644
--- a/tests/lean/run/dep_subst.lean
+++ b/tests/lean/run/dep_subst.lean
@@ -10,7 +10,7 @@ begin
   exact finset.card fxs
 end
 
-example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+example {T : Type} (xs : set T) [fn₁ : finite_set xs] [fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
 begin
   induction fn₁ with fxs₁ h₁,
   induction fn₂ with fxs₂ h₂,
@@ -18,7 +18,7 @@ begin
   apply sorry
 end
 
-example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+example {T : Type} (xs : set T) [fn₁ : finite_set xs] [fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
 begin
   induction fn₁ with fxs₁ h₁,
   induction fn₂ with fxs₂ h₂,
diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean
index 8e8b6275e..3b8b79674 100644
--- a/tests/lean/run/t1.lean
+++ b/tests/lean/run/t1.lean
@@ -4,7 +4,7 @@ print raw ((Prop))
 print raw Prop
 print raw fun (x y : Prop), x x
 print raw fun (x y : Prop) {z : Prop}, x y
-print raw λ [x y : Prop] {z : Prop}, x z
+print raw λ [x : Prop] [y : Prop] {z : Prop}, x z
 print raw Pi (x y : Prop) {z : Prop}, x
 print raw ∀ (x y : Prop) {z : Prop}, x
 print raw forall {x y : Prop} w {z : Prop}, x