diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2858847ef..957e2a62e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -159,7 +159,7 @@ public:
         auto ss = unify_simple(m_subst, c);
         m_subst = ss.second;
         if (ss.first == unify_status::Failed)
-            throw unifier_exception(c.get_justification());
+            throw unifier_exception(c.get_justification(), m_subst);
     }
 
     /**
diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp
index 023dbf272..145e79d75 100644
--- a/src/library/error_handling/error_handling.cpp
+++ b/src/library/error_handling/error_handling.cpp
@@ -11,10 +11,8 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/for_each_fn.h"
 #include "library/io_state_stream.h"
-// #include "library/elaborator/elaborator_justification.h"
-// #include "library/elaborator/elaborator_exception.h"
+#include "library/unifier.h"
 #include "library/parser_nested_exception.h"
-// #include "library/unsolved_metavar_exception.h"
 
 namespace lean {
 void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
@@ -51,13 +49,12 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
     ios << " " << ex << endl;
 }
 
-// static void display_error(io_state_stream const & ios, pos_info_provider const * p, elaborator_exception const & ex) {
-//     formatter fmt = ios.get_formatter();
-//     options opts  = ios.get_options();
-//     auto j = ex.get_justification();
-//     j = remove_detail(j);
-//     ios << mk_pair(j.pp(fmt, opts, p, true), opts) << endl;
-// }
+static void display_error(io_state_stream const & ios, pos_info_provider const * p, unifier_exception const & ex) {
+    formatter fmt = ios.get_formatter();
+    options opts  = ios.get_options();
+    auto j = ex.get_justification();
+    ios << mk_pair(j.pp(fmt, opts, p, ex.get_substitution()), opts) << endl;
+}
 
 // struct delta_pos_info_provider : public pos_info_provider {
 //     unsigned m_delta;
@@ -132,37 +129,11 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
 //     ios << ex.what() << endl;
 // }
 
-// static void display_error(io_state_stream const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) {
-//     display_error_pos(ios, p, ex.get_expr());
-//     formatter fmt = ios.get_formatter();
-//     options opts  = ios.get_options();
-//     unsigned indent = get_pp_indent(opts);
-//     format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts)));
-//     ios << " " << ex.what() << mk_pair(r, opts) << endl;
-//     if (p) {
-//         name_set already_displayed;
-//         for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool {
-//                 if (is_metavar(e)) {
-//                     name const & m = metavar_name(e);
-//                     if (already_displayed.find(m) == already_displayed.end()) {
-//                         already_displayed.insert(m);
-//                         for (unsigned i = 0; i < indent; i++) ios << " ";
-//                         display_error_pos(ios, p, e);
-//                         ios << " unsolved metavar " << m << endl;
-//                     }
-//                 }
-//                 return true;
-//             });
-//     }
-// }
-
 void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex) {
     if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
         display_error(ios, p, *k_ex);
-    // } else if (auto e_ex = dynamic_cast<elaborator_exception const *>(&ex)) {
-    //     display_error(ios, p, *e_ex);
-    // } else if (auto m_ex = dynamic_cast<unsolved_metavar_exception const *>(&ex)) {
-    //     display_error(ios, p, *m_ex);
+    } else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
+        display_error(ios, p, *e_ex);
     } else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {
         display_error(ios, p, *ls_ex);
     } else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) {
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index bf546cc1d..ce262daed 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -708,7 +708,7 @@ struct unifier_fn {
     optional<substitution> failure() {
         lean_assert(in_conflict());
         if (m_use_exception)
-            throw unifier_exception(*m_conflict);
+            throw unifier_exception(*m_conflict, m_subst);
         else
             return optional<substitution>();
     }
diff --git a/src/library/unifier.h b/src/library/unifier.h
index 6156eeaa4..7f9b33121 100644
--- a/src/library/unifier.h
+++ b/src/library/unifier.h
@@ -60,11 +60,13 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
 
 class unifier_exception : public exception {
     justification m_jst;
+    substitution  m_subst;
 public:
-    unifier_exception(justification const & j):exception("unifier exception"), m_jst(j) {}
-    virtual exception * clone() const { return new unifier_exception(m_jst); }
+    unifier_exception(justification const & j, substitution const & s):exception("unifier exception"), m_jst(j), m_subst(s) {}
+    virtual exception * clone() const { return new unifier_exception(m_jst, m_subst); }
     virtual void rethrow() const { throw *this; }
     justification const & get_justification() const { return m_jst; }
+    substitution const & get_substitution() const { return m_subst; }
 };
 
 void open_unifier(lua_State * L);