diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 9766e79fa..9c5e63fa6 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -19,7 +19,7 @@ expr abstract(expr const & e, unsigned s, unsigned n, expr const * subst) {
                 while (i > 0) {
                     --i;
                     if (subst[i] == e)
-                        return some_expr(mk_var(offset + s + n - i - 1));
+                        return some_expr(copy_tag(e, mk_var(offset + s + n - i - 1)));
                 }
             }
             return none_expr();
@@ -36,7 +36,7 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) {
                 while (i > 0) {
                     --i;
                     if (is_eqp(s[i], e))
-                        return some_expr(mk_var(offset + n - i - 1));
+                        return some_expr(copy_tag(e, mk_var(offset + n - i - 1)));
                 }
             }
             return none_expr();
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 030ffe514..43f26c85b 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -463,7 +463,7 @@ unsigned get_free_var_range(expr const & e) {
 bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); }
 bool is_bi_equal(expr const & a, expr const & b) { return expr_eq_fn(true)(a, b); }
 
-static expr copy_tag(expr const & e, expr && new_e) {
+expr copy_tag(expr const & e, expr && new_e) {
     tag t = e.get_tag();
     if (t != nulltag)
         new_e.set_tag(t);
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index c91284cfe..70f0f6ac5 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -149,6 +149,8 @@ public:
                     expr const & a7, expr const & a8) const;
 };
 
+expr copy_tag(expr const & e, expr && new_e);
+
 // =======================================
 // Structural equality
 /** \brief Binder information is ignored in the following predicate */