diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 75d00a8d7..6e94b47fb 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -104,7 +104,6 @@ struct print_axioms_deps {
         if (!m_use_axioms)
             m_ios << "no axioms" << endl;
     }
-
 };
 
 static void print_axioms(parser & p) {
diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out
index e62ea1048..1ac0772a3 100644
--- a/tests/lean/print_ax1.lean.expected.out
+++ b/tests/lean/print_ax1.lean.expected.out
@@ -1 +1,2 @@
-no axioms
+quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
+propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index a109893ac..da3bfe503 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,2 +1,4 @@
+quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
 em : ∀ (a : Prop), a ∨ ¬a
+propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}