diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index def4ccf065..8d51ef832b 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -10,3 +10,14 @@ import Lean.Parser.Tactic
 import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
+
+namespace Lean
+namespace Parser
+
+-- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
+@[export lean_mk_antiquot_parenthesizer]
+def mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : PrettyPrinter.Parenthesizer :=
+mkAntiquot.parenthesizer name kind anonymous
+
+end Parser
+end Lean
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 731ae7d267..b4df00904e 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -210,7 +210,7 @@ catch p1 $ fun e => match e with
 -- Note that there is a mutual recursion
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
---@[extern "lean_mk_antiquot_parenthesizer"]
+@[extern 7 "lean_mk_antiquot_parenthesizer"]
 constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer :=
 arbitrary _