diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index d8ae68047..abd7e4e2a 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -8,15 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-/** \brief Object to simulate delayed justification creation. */
-class delayed_justification {
-    optional<justification>        m_jst;
-    std::function<justification()> m_mk;
-public:
-    template<typename Mk> delayed_justification(Mk && mk):m_mk(mk) {}
-    justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
-};
-
 /** \brief Auxiliary exception used to sign that constraints cannot be created when \c m_cnstrs_enabled flag is false. */
 struct add_cnstr_exception {};
 
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index 66216245a..e95ef1ae5 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -140,4 +140,13 @@ bool depends_on(justification const & j, unsigned i);
 
 /** \brief Printer for debugging purposes */
 std::ostream & operator<<(std::ostream & out, justification const & j);
+
+/** \brief Object to simulate delayed justification creation. */
+class delayed_justification {
+    optional<justification>        m_jst;
+    std::function<justification()> m_mk;
+public:
+    template<typename Mk> delayed_justification(Mk && mk):m_mk(mk) {}
+    justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
+};
 }