diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index e2e8e654e9..592cee455c 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -280,6 +280,9 @@ fun stx => match_syntax stx with
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic paren] def evalParen : Tactic :=
+fun stx => evalTactic (stx.getArg 1)
+
 @[builtinTactic nestedTacticBlock] def evalNestedTacticBlock : Tactic :=
 fun stx => focus stx (evalTactic (stx.getArg 1))