diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 2de1d48f6..23ce36787 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -562,7 +562,7 @@ class elaborator::imp { if (is_var(a)) { auto e = find(ctx, var_idx(a)); if (e && e->get_body()) - a = *(e->get_body()); + a = lift_free_vars(*(e->get_body()), var_idx(a) + 1, m_state.m_menv); } } diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 4a7ab2a9c..f3d0122a0 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -633,11 +633,12 @@ void tst19() { void tst20() { std::cout << "\nTST 20\n"; environment env; + import_all(env); metavar_env menv; - expr N = Const("N"); - expr M = Const("M"); - env->add_var("N", Type()); - env->add_var("M", Type()); + expr N = Const("N1"); + expr M = Const("M1"); + env->add_var("N1", Type()); + env->add_var("M1", Type()); env->add_var("f", N >> (M >> M)); env->add_var("a", N); env->add_var("b", M);