diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 00115a7f09..24432e1c80 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -192,15 +192,12 @@ match s with
 
 end ParserState
 
-inductive ParserKind
-| leading | trailing
-
-export ParserKind (leading trailing)
-
 def ParserArg : ParserKind → Type
 | ParserKind.leading => Nat
 | ParserKind.trailing => Syntax
 
+export ParserKind (leading trailing)
+
 def BasicParserFn := ParserContext → ParserState → ParserState
 
 def ParserFn (k : ParserKind) := ParserArg k → BasicParserFn
diff --git a/src/Init/LeanExt.lean b/src/Init/LeanExt.lean
index edc3d3bcef..15e118d72e 100644
--- a/src/Init/LeanExt.lean
+++ b/src/Init/LeanExt.lean
@@ -23,10 +23,13 @@ inductive Name
 | str : Name → String → USize → Name
 | num : Name → Nat → USize → Name
 
+inductive ParserKind
+| leading | trailing
+
 /-
   Small DSL for describing parsers. We implement an interpreter for it
   at `Parser.lean` -/
-inductive ParserDescr
+inductive ParserDescr (kind : ParserKind := ParserKind.leading)
 | andthen       : ParserDescr → ParserDescr → ParserDescr
 | orelse        : ParserDescr → ParserDescr → ParserDescr
 | optional      : ParserDescr → ParserDescr