diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index d3bca66a30..6821abcc3c 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -78,10 +78,10 @@ bool contains_local(expr const & e, name const & n) {
     return result;
 }
 
-bool depends_on(unsigned sz, expr const * es, expr const & h) {
+optional<expr> depends_on(unsigned sz, expr const * es, expr const & h) {
     for (unsigned i = 0; i < sz; i++)
         if (depends_on(es[i], h))
-            return true;
-    return false;
+            return some_expr(es[i]);
+    return none_expr();
 }
 }
diff --git a/src/library/locals.h b/src/library/locals.h
index 14895fdc1c..e985778c01 100644
--- a/src/library/locals.h
+++ b/src/library/locals.h
@@ -35,5 +35,5 @@ inline bool depends_on(expr const & e, expr const & h) {
 }
 
 /** \brief Return true iff one of \c es contains the local constant \c h */
-bool depends_on(unsigned sz, expr const * es, expr const & h);
+optional<expr> depends_on(unsigned sz, expr const * es, expr const & h);
 }