diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp
index cda7e3ffd..87f0b1b5c 100644
--- a/src/library/abbreviation.cpp
+++ b/src/library/abbreviation.cpp
@@ -112,7 +112,7 @@ expr expand_abbreviations(environment const & env, expr const & e) {
     abbrev_state const & s = abbrev_ext::get_state(env);
     return replace(e, [&](expr const & e, unsigned) {
             if (is_constant(e) && s.is_abbreviation(const_name(e)))
-                return some_expr(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e)));
+                return some_expr(try_eta(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e))));
             else
                 return none_expr();
         });