diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index e1922e9a4d..76b03a977b 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -296,7 +296,8 @@ class MonadQuotation (m : Type → Type) :=
    transformer and not just a monadic action ensures that the current macro
    scope before the recursive call is restored after it, as expected. -/
 (withFreshMacroScope {α : Type} : m α → m α)
-export MonadQuotation
+
+export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
 /-
 We represent a name with macro scopes as
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 5ccc1c5ad9..03adc4ff4a 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -28,7 +28,7 @@ let newAlts ← alts.mapSepElemsM fun alt => do
     let newHole ← `(?$holeName:ident)
     modify fun s => { s with nextIdx := s.nextIdx + 1}
     pure $ alt.setArg 2 newHole
-  else MonadQuotation.withFreshMacroScope do -- TODO: why do we need MonadQuotation here
+  else withFreshMacroScope do
     let newHole ← `(?rhs)
     let newHoleId := newHole.getArg 1
     let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
@@ -39,7 +39,7 @@ let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
 pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
-let (matchTerm, s) ← (mkAuxiliaryMatchTermAux parentTag matchTac).run {}
+let (matchTerm, s) ← mkAuxiliaryMatchTermAux parentTag matchTac $.run {}
 pure (matchTerm, s.cases)
 
 @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=