diff --git a/src/util/list.h b/src/util/list.h
index 996704fa84..ae23a8f4fe 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -133,4 +133,12 @@ template<typename It> list<typename std::iterator_traits<It>::value_type> to_lis
     }
     return r;
 }
+
+/** \brief Return <tt>reverse(to_list(begin, end))</tt> */
+template<typename It> list<typename std::iterator_traits<It>::value_type> reverse_to_list(It const & begin, It const & end) {
+    list<typename std::iterator_traits<It>::value_type> r;
+    for (auto it = begin; it != end; ++it)
+        r = cons(*it, r);
+    return r;
+}
 }
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index 87175c08e2..bf42f28040 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -60,6 +60,26 @@ std::pair<list<T>, list<T>> split(list<T> const & l) {
     }
 }
 
+/**
+   \brief Return two lists \c l1 and \c l2 of approximately the same size s.t.
+   <tt>append(l1, reverse(l2)) == l</tt>
+*/
+template<typename T>
+std::pair<list<T>, list<T>> split_reverse_second(list<T> const & l) {
+    if (is_nil(l)) {
+        return mk_pair(l, l);
+    } else if (is_nil(cdr(l))) {
+        return mk_pair(l, list<T>());
+    } else {
+        buffer<T> tmp;
+        to_buffer(l, tmp);
+        unsigned mid = tmp.size() / 2;
+        auto beg = tmp.begin();
+        lean_assert(beg + mid <= tmp.end());
+        return mk_pair(to_list(beg, beg + mid), reverse_to_list(beg+mid, tmp.end()));
+    }
+}
+
 /**
    \brief Append two lists
 */
diff --git a/src/util/queue.h b/src/util/queue.h
index 025f3aac76..5d3d2edc93 100644
--- a/src/util/queue.h
+++ b/src/util/queue.h
@@ -45,8 +45,7 @@ public:
             if (is_nil(cdr(q.m_rear))) {
                 return mk_pair(queue(), car(q.m_rear));
             } else {
-                auto p = split(q.m_rear);
-                p.second = reverse(p.second);
+                auto p = split_reverse_second(q.m_rear);
                 return mk_pair(queue(cdr(p.second), p.first), car(p.second));
             }
         } else {
@@ -66,8 +65,7 @@ public:
             if (is_nil(cdr(q.m_front))) {
                 return mk_pair(queue(), car(q.m_front));
             } else {
-                auto p = split(q.m_front);
-                p.second = reverse(p.second);
+                auto p = split_reverse_second(q.m_front);
                 return mk_pair(queue(p.first, cdr(p.second)), car(p.second));
             }
         } else {