diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 44c127db3c..b2347f6a7c 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -3505,8 +3505,9 @@ environment load_external_fn(environment & env, name const & extern_n) {
     }
 }
 
-[[noreturn]] void vm_check_failed(char const *fn, unsigned line, char const *msg) {
-    throw exception(sstream() << "VM check failed at " << fn << ":" << line << ": " << msg);
+[[noreturn]] void vm_check_failed(char const * condition) {
+    throw exception(sstream() << "vm check failed: " << condition
+                              << " (possibly due to incorrect axioms, or sorry)");
 }
 
 class vm_index_manager {
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index e14df7f063..ebabc1b48f 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -58,11 +58,11 @@ public:
 #define LEAN_ALWAYS_INLINE
 #endif
 
-[[noreturn]] void vm_check_failed(char const * fn, unsigned line, char const * msg);
+[[noreturn]] void vm_check_failed(char const * condition);
 #if defined(LEAN_VM_UNCHECKED)
 #define lean_vm_check(cond) lean_assert(cond)
 #else
-#define lean_vm_check(cond) { if (LEAN_UNLIKELY(!(cond))) vm_check_failed(__FILE__, __LINE__, #cond); }
+#define lean_vm_check(cond) { if (LEAN_UNLIKELY(!(cond))) vm_check_failed(#cond); }
 #endif
 
 void display(std::ostream & out, vm_obj const & o);