diff --git a/src/library/scope.cpp b/src/library/scope.cpp
index dcbc92b96..73b9fb4c3 100644
--- a/src/library/scope.cpp
+++ b/src/library/scope.cpp
@@ -90,7 +90,7 @@ public:
                         if (info.m_local) {
                             return some_expr(update_constant(e, levels()));
                         } else {
-                            return some_expr(mk_app(update_constant(e, append(const_levels(e), info.m_levels)), info.m_var_deps));
+                            return some_expr(mk_app(update_constant(e, append(info.m_levels, const_levels(e))), info.m_var_deps));
                         }
                     } else {
                         levels new_ls = map(const_levels(e), [&](level const & l) { return convert(l); });
@@ -176,7 +176,7 @@ public:
         expr new_type  = convert(d.get_type());
         expr new_value = convert(d.get_value());
         level_param_names level_deps = mk_level_deps();
-        level_param_names new_ls = append(d.get_params(), level_deps);
+        level_param_names new_ls = append(level_deps, d.get_params());
         dependencies var_deps    = mk_var_deps();
         new_type  = Pi(new_type, var_deps);
         new_value = Fun(new_value, var_deps);
diff --git a/tests/lua/sect1b.lua b/tests/lua/sect1b.lua
new file mode 100644
index 000000000..68d6f8c9e
--- /dev/null
+++ b/tests/lua/sect1b.lua
@@ -0,0 +1,12 @@
+local env = environment()
+env = env:begin_section_scope()
+env = env:add_global_level("l")
+local l  = mk_global_univ("l")
+local l1 = mk_param_univ("l1")
+env = add_decl(env, mk_definition("A", {l1}, mk_sort(max_univ(l, l1)+1), mk_sort(max_univ(l, l1))))
+env = env:end_scope()
+local ls = env:find("A"):univ_params()
+assert(#ls == 2)
+print(ls:head())
+assert(ls:head() == name("l"))
+assert(ls:tail():head() == name("l1"))