diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
index 04609a8cba..a7fc71284e 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
@@ -53,10 +53,8 @@ def elabMPure : Tactic
     replaceMainGoal [m.mvarId!]
   | _ => throwUnsupportedSyntax
 
-macro "mpure_intro" : tactic => `(tactic| apply Pure.intro)
-
 def MGoal.triviallyPure (goal : MGoal) : OptionT MetaM Expr := do
   let mv ← mkFreshExprMVar goal.toExpr
-  let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply Pure.intro; trivial)) catch _ => failure
+  let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); trivial)) catch _ => failure
     | failure
   return mv