diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean
index 3f8f844a7b..79e62e61ac 100644
--- a/src/Lean/Meta/Tactic/Revert.lean
+++ b/src/Lean/Meta/Tactic/Revert.lean
@@ -43,6 +43,7 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
       finally
         mvarId.setKind .syntheticOpaque
     let mvar := e.getAppFn
+    mvar.mvarId!.setKind .syntheticOpaque
     mvar.mvarId!.setTag tag
     return (toRevert.map Expr.fvarId!, mvar.mvarId!)
 
diff --git a/tests/lean/run/revertMetavarKind.lean b/tests/lean/run/revertMetavarKind.lean
new file mode 100644
index 0000000000..56137b95e5
--- /dev/null
+++ b/tests/lean/run/revertMetavarKind.lean
@@ -0,0 +1,10 @@
+import Lean.Meta
+
+open Lean Elab Tactic
+
+example (n : Nat) : n = n := by
+  revert n
+  run_tac do
+    guard (← getMainDecl).kind.isSyntheticOpaque
+  intro n
+  rfl