diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index f894f8d9dd..79397a1619 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1817,54 +1817,6 @@ def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
 def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
   { fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s }
 
-unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s =>
-  match ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.Parser declName <|>
-        ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.TrailingParser declName with
-  | Except.ok p    => p.fn ctx s
-  | Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}"
-
-@[implementedBy evalParserConstUnsafe]
-constant evalParserConst (declName : Name) : ParserFn
-
-unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
-  let stack := s.stxStack
-  if stack.size < offset + 1 then
-    s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
-  else
-    match stack.get! (stack.size - offset - 1) with
-    | Syntax.ident (val := parserName) .. =>
-      match ctx.resolveName parserName with
-      | [(parserName, [])] =>
-        let iniSz := s.stackSize
-        let s := evalParserConst parserName ctx s
-        if !s.hasError && s.stackSize != iniSz + 1 then
-          s.mkUnexpectedError "expected parser to return exactly one syntax object"
-        else
-          s
-      | _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
-      | _ => s.mkUnexpectedError s!"unknown parser {parserName}"
-    | _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
-
-@[implementedBy parserOfStackFnUnsafe]
-constant parserOfStackFn (offset : Nat) : ParserFn
-
-def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
-  { fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
-
-register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
-  defValue := false
-  group    := "internal"
-  descr    := "(Lean bootstrapping) use parsers from the current stage inside quotations"
-}
-
-/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
-def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
-  fn := fun c s =>
-    if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
-      evalParserConst declName c s
-    else
-      p.fn c s }
-
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index c660225c17..9c7bc620b1 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -147,20 +147,6 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
   | Except.ok tokenTable => builtinTokenTable.set tokenTable
   | Except.error msg     => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
 
-def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
-  let p := evalInsideQuot declName p
-  let categories ← builtinParserCategoriesRef.get
-  let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
-  builtinParserCategoriesRef.set categories
-  builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
-  updateBuiltinTokens p.info declName
-
-def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
-  addBuiltinParser catName declName true p prio
-
-def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
-  addBuiltinParser catName declName false p prio
-
 def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
   match e with
   | Entry.token tk =>
@@ -178,34 +164,6 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
     | Except.ok categories => { s with categories := categories }
     | _ => unreachable!
 
-unsafe def mkParserOfConstantUnsafe
-    (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
-  let env  := (← read).env
-  let opts := (← read).opts
-  match env.find? constName with
-  | none      => throw ↑s!"unknow constant '{constName}'"
-  | some info =>
-    match info.type with
-    | Expr.const `Lean.Parser.TrailingParser _ _ =>
-      let p ← IO.ofExcept $ env.evalConst Parser opts constName
-      pure ⟨false, p⟩
-    | Expr.const `Lean.Parser.Parser _ _ =>
-      let p ← IO.ofExcept $ env.evalConst Parser opts constName
-      pure ⟨true, p⟩
-    | Expr.const `Lean.ParserDescr _ _ =>
-      let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
-      let p ← compileParserDescr d
-      pure ⟨true, p⟩
-    | Expr.const `Lean.TrailingParserDescr _ _ =>
-      let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
-      let p ← compileParserDescr d
-      pure ⟨false, p⟩
-    | _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
-
-@[implementedBy mkParserOfConstantUnsafe]
-constant mkParserOfConstantAux
-    (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
-
 /- Parser aliases for making `ParserDescr` extensible -/
 inductive AliasValue (α : Type) where
   | const  (p : α)
@@ -268,6 +226,32 @@ def ensureBinaryParserAlias (aliasName : Name) : IO Unit :=
 def ensureConstantParserAlias (aliasName : Name) : IO Unit :=
   discard $ getConstAlias parserAliasesRef aliasName
 
+unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
+  let env  := (← read).env
+  let opts := (← read).opts
+  match env.find? constName with
+  | none      => throw ↑s!"unknow constant '{constName}'"
+  | some info =>
+    match info.type with
+    | Expr.const `Lean.Parser.TrailingParser _ _ =>
+      let p ← IO.ofExcept $ env.evalConst Parser opts constName
+      pure ⟨false, p⟩
+    | Expr.const `Lean.Parser.Parser _ _ =>
+      let p ← IO.ofExcept $ env.evalConst Parser opts constName
+      pure ⟨true, p⟩
+    | Expr.const `Lean.ParserDescr _ _ =>
+      let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
+      let p ← compileParserDescr d
+      pure ⟨true, p⟩
+    | Expr.const `Lean.TrailingParserDescr _ _ =>
+      let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
+      let p ← compileParserDescr d
+      pure ⟨false, p⟩
+    | _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
+
+@[implementedBy mkParserOfConstantUnsafe]
+constant mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
+
 partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
   let rec visit : ParserDescr → ImportM Parser
     | ParserDescr.const n                             => getConstAlias parserAliasesRef n
@@ -281,7 +265,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
     | ParserDescr.symbol tk                           => return symbol tk
     | ParserDescr.nonReservedSymbol tk includeIdent   => return nonReservedSymbol tk includeIdent
     | ParserDescr.parser constName                    => do
-      let (_, p) ← mkParserOfConstantAux categories constName visit;
+      let (_, p) ← mkParserOfConstantAux constName visit;
       pure p
     | ParserDescr.cat catName prec                    =>
       match getCategory categories catName with
@@ -290,7 +274,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
   visit d
 
 def mkParserOfConstant (categories : ParserCategories) (constName : Name) : ImportM (Bool × Parser) :=
-  mkParserOfConstantAux categories constName (compileParserDescr categories)
+  mkParserOfConstantAux constName (compileParserDescr categories)
 
 structure ParserAttributeHook where
   /- Called after a parser attribute is applied to a declaration. -/
@@ -354,6 +338,43 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
   | none     => LeadingIdentBehavior.default
   | some cat => cat.behavior
 
+unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
+  let categories := (parserExtension.getState ctx.env).categories
+  match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
+  | Except.ok (bool, p) => p.fn ctx s
+  | Except.error e => s.mkUnexpectedError e.toString
+
+@[implementedBy evalParserConstUnsafe]
+constant evalParserConst (declName : Name) : ParserFn
+
+register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
+  defValue := false
+  group    := "internal"
+  descr    := "(Lean bootstrapping) use parsers from the current stage inside quotations"
+}
+
+/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
+def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
+  fn := fun c s =>
+    if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
+      evalParserConst declName c s
+    else
+      p.fn c s }
+
+def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
+  let p := evalInsideQuot declName p
+  let categories ← builtinParserCategoriesRef.get
+  let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
+  builtinParserCategoriesRef.set categories
+  builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
+  updateBuiltinTokens p.info declName
+
+def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
+  addBuiltinParser catName declName true p prio
+
+def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
+  addBuiltinParser catName declName false p prio
+
 def mkCategoryAntiquotParser (kind : Name) : Parser :=
   mkAntiquot kind.toString none
 
@@ -606,5 +627,27 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
   fn   := withOpenDeclFn  p.fn
 }
 
+def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
+  let stack := s.stxStack
+  if stack.size < offset + 1 then
+    s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
+  else
+    match stack.get! (stack.size - offset - 1) with
+    | Syntax.ident (val := parserName) .. =>
+      match ctx.resolveName parserName with
+      | [(parserName, [])] =>
+        let iniSz := s.stackSize
+        let s := evalParserConst parserName ctx s
+        if !s.hasError && s.stackSize != iniSz + 1 then
+          s.mkUnexpectedError "expected parser to return exactly one syntax object"
+        else
+          s
+      | _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
+      | _ => s.mkUnexpectedError s!"unknown parser {parserName}"
+    | _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
+
+def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
+  { fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
+
 end Parser
 end Lean
diff --git a/tests/lean/run/syntaxAbbrevQuot.lean b/tests/lean/run/syntaxAbbrevQuot.lean
new file mode 100644
index 0000000000..3e0e415c8d
--- /dev/null
+++ b/tests/lean/run/syntaxAbbrevQuot.lean
@@ -0,0 +1,6 @@
+syntax foo := "a" <|> "b"
+
+syntax "bla" foo : term -- TODO: necessary to declare a and b as keywords
+
+#check `(foo| a)
+#check (· matches `(foo| a))