diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 8c492974a3..b5b561a09a 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1004,6 +1004,15 @@ void vm_state::invoke_builtin(vm_decl const & d) {
 
 LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr);
 
+scope_vm_state::scope_vm_state(vm_state & s):
+    m_prev(g_vm_state) {
+    g_vm_state = &s;
+}
+
+scope_vm_state::~scope_vm_state() {
+    g_vm_state = m_prev;
+}
+
 void vm_state::invoke_cfun(vm_decl const & d) {
     flet<vm_state *> Set(g_vm_state, this);
     auto & S       = m_stack;
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 9ade0e3d30..e8368a48a7 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -583,6 +583,14 @@ public:
     }
 };
 
+/** \brief Helper class for setting thread local vm_state object */
+class scope_vm_state {
+    vm_state * m_prev;
+public:
+    scope_vm_state(vm_state & s);
+    ~scope_vm_state();
+};
+
 /** \brief Return reference to thread local VM state object. */
 vm_state const & get_vm_state();