diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp
index abbae5ca8..22652804c 100644
--- a/src/library/abbreviation.cpp
+++ b/src/library/abbreviation.cpp
@@ -109,7 +109,7 @@ expr expand_abbreviations(environment const & env, expr const & e) {
         return e;
     abbrev_state const & s = abbrev_ext::get_state(env);
     return replace(e, [&](expr const & e, unsigned) {
-            if (s.is_abbreviation(const_name(e)))
+            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)));
             else
                 return none_expr();