diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
index 2ae2bef354..61056dbd27 100644
--- a/src/Init/Lean/Elab/Tactic.lean
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -13,7 +13,7 @@ namespace Elab
 namespace Term
 
 def mkTacticMVar (ref : Syntax) (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
-mvar ← mkFreshExprMVar ref type MetavarKind.synthetic `main;
+mvar ← mkFreshExprMVar ref type MetavarKind.syntheticOpaque `main;
 let mvarId := mvar.mvarId!;
 registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode;
 pure mvar
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 62ad418433..8a6a3d483b 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -641,7 +641,7 @@ fun stx expectedType? => mkFreshExprMVar stx expectedType?
 @[builtinTermElab «namedHole»] def elabNamedHole : TermElab :=
 fun stx expectedType? =>
   let name := stx.getIdAt 1;
-  mkFreshExprMVar stx expectedType? MetavarKind.synthetic name
+  mkFreshExprMVar stx expectedType? MetavarKind.syntheticOpaque name
 
 /-- Main loop for `mkPairs`. -/
 private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syntax