diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index fd0ab1d50..9b6f0562b 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -39,6 +39,13 @@ bool justification::has_children() const {
     return !r.empty();
 }
 
+assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
+void assumption_justification::get_children(buffer<justification_cell*> &) const {}
+expr const & assumption_justification::get_main_expr() const { return expr::null(); }
+format assumption_justification::pp_header(formatter const &, options const &) const {
+    return format{format("assumption"), space(), format(m_idx)};
+}
+
 bool depends_on(justification const & t, justification const & d) {
     buffer<justification_cell *>   todo;
     buffer<justification_cell *>   children;
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index e8388f282..1e1271442 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -37,6 +37,18 @@ public:
     bool is_shared() const { return get_rc() > 1; }
 };
 
+/**
+   \brief Base class for justification objects used to justify case-splits.
+*/
+class assumption_justification : public justification_cell {
+    unsigned m_idx;
+public:
+    assumption_justification(unsigned idx);
+    virtual void get_children(buffer<justification_cell*> &) const;
+    virtual expr const & get_main_expr() const;
+    virtual format pp_header(formatter const &, options const &) const;
+};
+
 /**
    \brief Smart pointer for justification_cell's
 */
@@ -66,6 +78,8 @@ public:
     bool has_children() const;
 };
 
+inline justification mk_assumption_justification(unsigned idx) { return justification(new assumption_justification(idx)); }
+
 /**
    \brief Return true iff \c t depends on \c d.
    That is \c t is a descendant of \c d.
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 5a4f3b8ca..10e91459e 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -164,7 +164,7 @@ class elaborator::imp {
     justification mk_assumption() {
         unsigned id = m_next_id;
         m_next_id++;
-        return justification(new assumption_justification(id));
+        return mk_assumption_justification(id);
     }
 
     /** \brief Add given constraint to the front of the current constraint queue */
diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp
index 368d5f7b5..de082692b 100644
--- a/src/library/elaborator/elaborator_justification.cpp
+++ b/src/library/elaborator/elaborator_justification.cpp
@@ -18,20 +18,6 @@ static void append(buffer<justification_cell*> & r, T const & s) {
         push_back(r, t);
 }
 
-// -------------------------
-// Assumptions
-// -------------------------
-assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {
-}
-void assumption_justification::get_children(buffer<justification_cell*> &) const {
-}
-expr const & assumption_justification::get_main_expr() const {
-    return expr::null();
-}
-format assumption_justification::pp_header(formatter const &, options const &) const {
-    return format{format("assumption"), space(), format(m_idx)};
-}
-
 // -------------------------
 // Propagation justification
 // -------------------------
diff --git a/src/library/elaborator/elaborator_justification.h b/src/library/elaborator/elaborator_justification.h
index 87c4586a5..fd33a019c 100644
--- a/src/library/elaborator/elaborator_justification.h
+++ b/src/library/elaborator/elaborator_justification.h
@@ -9,18 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/unification_constraint.h"
 
 namespace lean {
-/**
-   \brief Base class for justification objects used to justify case-splits.
-*/
-class assumption_justification : public justification_cell {
-    unsigned m_idx;
-public:
-    assumption_justification(unsigned idx);
-    virtual void get_children(buffer<justification_cell*> &) const;
-    virtual expr const & get_main_expr() const;
-    virtual format pp_header(formatter const &, options const &) const;
-};
-
 /**
    \brief Base class for justifying propagations and failures
 */