diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean
index d2470d1b2..b2163ab49 100644
--- a/tests/lean/run/alias1.lean
+++ b/tests/lean/run/alias1.lean
@@ -44,5 +44,5 @@ theorem T3 : aux2 = N2.foo (f a) (f b)
 
 
 check foo a b
-theorem T4 : foo a b = N1.foo a b
+theorem T4 : foo a b = N2.foo a b
 := refl _
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 051a1ff5e..03e50fb86 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -49,8 +49,8 @@ theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabite
 inhabited_mk (inr A (default B))
 
 theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B)
-  (H1 : ∀a1 a2, decidable (inl B a1 = inl B a2))
-  (H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
+  (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
+  (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
 rec_on s1
   (take a1, show decidable (inl B a1 = s2), from
     rec_on s2