diff --git a/tests/lean/print_ax2.lean b/tests/lean/print_ax2.lean
deleted file mode 100644
index efdcf5db5e..0000000000
--- a/tests/lean/print_ax2.lean
+++ /dev/null
@@ -1 +0,0 @@
-open subtype print axioms
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
deleted file mode 100644
index 85a3793d7f..0000000000
--- a/tests/lean/print_ax2.lean.expected.out
+++ /dev/null
@@ -1,2 +0,0 @@
-print_ax2.lean:1:13: error: invalid namespace name 'print'
-print_ax2.lean:1:25: error: invalid variables/constants/axioms declaration, ':' expected