diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp
index ece1f2da6..b2991c84d 100644
--- a/src/library/abstract_expr_manager.cpp
+++ b/src/library/abstract_expr_manager.cpp
@@ -5,6 +5,7 @@ Author: Daniel Selsam
 */
 #include "library/abstract_expr_manager.h"
 #include "util/safe_arith.h"
+#include "util/list_fn.h"
 
 namespace lean {
 
@@ -15,11 +16,11 @@ unsigned abstract_expr_manager::get_weight(expr const & e) {
     case expr_kind::Meta:
     case expr_kind::Sort:
     case expr_kind::Var:
-    case expr_kind::Macro:        
+    case expr_kind::Macro:
         return ::lean::get_weight(e);
     case expr_kind::Lambda:
-    case expr_kind::Pi:        
-        return safe_add(1,safe_add(get_weight(binding_domain(e)), get_weight(binding_body(e))));
+    case expr_kind::Pi:
+        return safe_add(1, safe_add(get_weight(binding_domain(e)), get_weight(binding_body(e))));
     case expr_kind::App:
         buffer<expr> args;
         expr f = get_app_args(e, args);
@@ -45,10 +46,10 @@ unsigned abstract_expr_manager::hash(expr const & e) {
     case expr_kind::Meta:
     case expr_kind::Sort:
     case expr_kind::Var:
-    case expr_kind::Macro:        
+    case expr_kind::Macro:
         return e.hash();
     case expr_kind::Lambda:
-    case expr_kind::Pi:        
+    case expr_kind::Pi:
         return ::lean::hash(hash(binding_domain(e)), hash(binding_body(e)));
     case expr_kind::App:
         buffer<expr> args;
@@ -114,7 +115,7 @@ bool abstract_expr_manager::is_lt(expr const & a, expr const & b) {
     if (wa < wb)                         return true;
     if (wa > wb)                         return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
-    if (is_equal(a,b))                   return false;
+    if (is_equal(a, b))                  return false;
     switch (a.kind()) {
     case expr_kind::Var:
     case expr_kind::Constant:
diff --git a/src/library/abstract_expr_manager.h b/src/library/abstract_expr_manager.h
index 83ebeb6a4..446e8e642 100644
--- a/src/library/abstract_expr_manager.h
+++ b/src/library/abstract_expr_manager.h
@@ -19,7 +19,7 @@ public:
         m_fun_info_manager(f_info_manager) { }
 
     unsigned get_weight(expr const & e);
-    unsigned hash(expr const & e);    
+    unsigned hash(expr const & e);
     bool is_equal(expr const & a, expr const & b);
     bool is_lt(expr const & a, expr const & b);
 };
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 092b99ee3..0fc610085 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -665,7 +665,7 @@ void finalize_simplifier() {
 
 /* Entry point */
 result simplify(name const & rel, expr const & e, simp_rule_sets const & srss) {
-    return simplifier(rel, srss)(e);    
+    return simplifier(rel, srss)(e);
 }
 
 }}
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index 38a2514c1..587eeb3e8 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -281,7 +281,7 @@ void for_each(list<T> const & l, F && f) {
     }
 }
 
-/** \brief Given lists <tt>(a_0, ..., a_k)</tt> and <tt>(b_0, ..., b_k)</tt>, 
+/** \brief Given lists <tt>(a_0, ..., a_k)</tt> and <tt>(b_0, ..., b_k)</tt>,
     exec f(a_0, b_0); f(a_1, b_1); ... f(a_k, b_k)</tt>. */
 template<typename T1, typename T2, typename F>
 void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
@@ -298,24 +298,24 @@ void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
     }
 }
 
-/** \brief Given lists <tt>(a_0, ..., a_k)</tt>, <tt>(b_0, ..., b_k)</tt>, 
-    and <tt>(c_0, ..., c_k)</tt>, 
+/** \brief Given lists <tt>(a_0, ..., a_k)</tt>, <tt>(b_0, ..., b_k)</tt>,
+    and <tt>(c_0, ..., c_k)</tt>,
     exec f(a_0, b_0, c_0); f(a_1, b_1, c_1); ... f(a_k, b_k, c_k)</tt>. */
 template<typename T1, typename T2, typename T3, typename F>
-void for_each2(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F && f) {
+void for_each3(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F && f) {
     static_assert(std::is_same<typename std::result_of<F(T1 const &, T2 const &, T3 const &)>::type, void>::value,
                   "for_each2: return type of f is not void");
     typedef typename list<T1>::cell cell1;
     typedef typename list<T2>::cell cell2;
-    typedef typename list<T3>::cell cell3;    
+    typedef typename list<T3>::cell cell3;
     cell1 * it1 = l1.raw();
     cell2 * it2 = l2.raw();
-    cell3 * it3 = l3.raw();    
+    cell3 * it3 = l3.raw();
     while (it1 && it2 && it3) {
         f(it1->head(), it2->head(), it3->head());
         it1 = it1->tail().raw();
         it2 = it2->tail().raw();
-        it3 = it3->tail().raw();        
+        it3 = it3->tail().raw();
     }
 }