diff --git a/tests/lean/print_ax2.lean b/tests/lean/print_ax2.lean
index e629bda5d..c1fffdd24 100644
--- a/tests/lean/print_ax2.lean
+++ b/tests/lean/print_ax2.lean
@@ -1,3 +1,3 @@
-import logic.axioms.hilbert logic.axioms.funext
+import logic.axioms.hilbert logic.axioms.em
 
 print axioms
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index 5e48dd6c0..bc4e73fef 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,2 +1,2 @@
-funext : ∀ {A : Type} {B : A → Type} {f g : Π (a : A), B a}, (∀ (a : A), f a = g a) → f = g
-strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A) | (∃ (y : A), P y) → P x }
+em : ∀ (a : Prop), a ∨ ¬a
+strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| (∃ (y : A), P y) → P x}
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 0650f3bb6..0a7466fbc 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -4,6 +4,7 @@ measurable : Type → Type
 nonempty : Type → Prop
 point : Type → Type → Type
 setoid : Type → Type
+subsingleton : Type → Prop
 well_founded : Π {A : Type}, (A → A → Prop) → Prop
 decidable : Prop → Type₁
 inhabited : Type → Type
@@ -11,4 +12,5 @@ measurable : Type → Type
 nonempty : Type → Prop
 point : Type → Type → Type
 setoid : Type → Type
+subsingleton : Type → Prop
 well_founded : Π {A : Type}, (A → A → Prop) → Prop