diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index f4b7a1c777..04b4e80c5c 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -528,5 +528,4 @@ except that it doesn't print an empty diagnostic.
 
 (This is effectively a synonym for `run_elab`.)
 -/
-macro (name := runMeta) "run_meta " elems:doSeq : command =>
-  `(command| run_elab (show MetaM Unit from do $elems))
+syntax (name := runMeta) "run_meta " doSeq : command
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index b6d6a46fb3..ab5213a54d 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -704,22 +704,37 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
+private def checkImportsForRunCmds : CommandElabM Unit := do
+  unless (← getEnv).contains ``CommandElabM do
+    throwError "to use this command, include `import Lean.Elab.Command`"
+
 @[builtin_command_elab runCmd]
 def elabRunCmd : CommandElab
   | `(run_cmd $elems:doSeq) => do
-    ← liftTermElabM <| Term.withDeclName `_run_cmd <|
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_cmd <|
       unsafe Term.evalTerm (CommandElabM Unit)
         (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(discard do $elems))
+        (← `(discard do $elems)))
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab runElab]
 def elabRunElab : CommandElab
   | `(run_elab $elems:doSeq) => do
-    ← liftTermElabM <| Term.withDeclName `_run_elab <|
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_elab <|
       unsafe Term.evalTerm (CommandElabM Unit)
         (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(Command.liftTermElabM <| discard do $elems))
+        (← `(Command.liftTermElabM <| discard do $elems)))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runMeta]
+def elabRunMeta : CommandElab := fun stx =>
+  match stx with
+  | `(run_meta $elems:doSeq) => do
+     checkImportsForRunCmds
+     let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
+     withMacroExpansion stx stxNew do elabCommand stxNew
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
diff --git a/tests/lean/run/run_meta1.lean b/tests/lean/run/run_meta1.lean
new file mode 100644
index 0000000000..d5bad4c74b
--- /dev/null
+++ b/tests/lean/run/run_meta1.lean
@@ -0,0 +1,8 @@
+import Lean.Elab.Command
+
+run_meta guard true
+
+open Lean Meta in
+run_meta do
+  let type ← inferType (mkConst ``true)
+  IO.println type
diff --git a/tests/lean/run_meta1.lean b/tests/lean/run_meta1.lean
new file mode 100644
index 0000000000..51d8227280
--- /dev/null
+++ b/tests/lean/run_meta1.lean
@@ -0,0 +1 @@
+run_meta guard true
diff --git a/tests/lean/run_meta1.lean.expected.out b/tests/lean/run_meta1.lean.expected.out
new file mode 100644
index 0000000000..77e37d99ee
--- /dev/null
+++ b/tests/lean/run_meta1.lean.expected.out
@@ -0,0 +1 @@
+run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Elab.Command`