From ec71dd256f9f0ada84c383281731ba6e400310dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Oct 2019 21:01:31 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/instuniv.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean
index 09c5cdcb65..65c3bc3d83 100644
--- a/tests/lean/run/instuniv.lean
+++ b/tests/lean/run/instuniv.lean
@@ -5,8 +5,8 @@ def tst : IO Unit :=
 do env ← importModules [`Init.Data.Array.Default];
    match env.find `Array.foldl with
    | some info => do
-     IO.println (info.instantiateTypeUnivParams [Level.zero, Level.zero]);
-     IO.println (info.instantiateValueUnivParams [Level.zero, Level.zero]);
+     IO.println (info.instantiateTypeLevelParams [Level.zero, Level.zero]);
+     IO.println (info.instantiateValueLevelParams [Level.zero, Level.zero]);
      pure ()
    | none      => IO.println ("Array.foldl not found");
    pure ()