diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 48b3cfb1fc..5e6973630a 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -335,6 +335,7 @@ environment vm_compile(environment const & env, buffer<pair<name, expr>> const &
 }
 
 environment vm_compile(environment const & env, declaration const & d) {
+    if (!d.is_definition()) return env;
     buffer<pair<name, expr>> procs;
     preprocess(env, d, procs);
     return vm_compile(env, procs);
diff --git a/tests/lean/run/declare_axiom.lean b/tests/lean/run/declare_axiom.lean
new file mode 100644
index 0000000000..cc8443f84b
--- /dev/null
+++ b/tests/lean/run/declare_axiom.lean
@@ -0,0 +1,5 @@
+open tactic
+
+run_command (do
+  e ← to_expr `(false),
+  add_decl $ declaration.ax `useful_assumption [] e)