diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index e8169d424c..89a1d91a4e 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -317,4 +317,9 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl;
   compileDecl decl
 
+def ImportM.runCoreM (x : CoreM α) : ImportM α := do
+  let ctx ← read
+  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
+  return a
+
 end Lean