diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index fd2e55993..8546d9396 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -315,6 +315,7 @@ format justification::pp_core(formatter const & fmt, pos_info_provider const * p
         format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false);
         return r1 + r2;
     }}
+    lean_unreachable();
 }
 
 format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const {