diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index 81afd505c..4a668fe04 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -60,6 +60,9 @@ public:
     void d_assign(level const & m, level const & t, justification const & j) { d_assign(meta_id(m), t, j); }
     void d_assign(level const & m, level const & t) { d_assign(m, t, justification ()); }
 
+    void d_forget_justifications() { m_expr_jsts  = jst_map(); m_level_jsts = jst_map(); }
+    substitution forget_justifications() const { substitution s(*this); s.d_forget_justifications(); return s; }
+
     template<typename F>
     void for_each_expr(F && fn) const {
         for_each(m_expr_subst, [=](name const & n, expr const & e) { fn(n, e, get_expr_jst(n)); });
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 5d1b65623..f43c4a8a0 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1156,7 +1156,7 @@ struct unifier_fn {
         }
         lean_assert(!in_conflict());
         lean_assert(m_cnstrs.empty());
-        return optional<substitution>(m_subst);
+        return optional<substitution>(m_subst.forget_justifications());
     }
 };