diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 28ef449c07..d6183dc10d 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1809,6 +1809,20 @@ mkAntiquot "fieldIdx" `fieldIdx <|>
 { fn   := fun _ => fieldIdxFn,
   info := mkAtomicInfo "fieldIdx" }
 
+/- Helper functions for defining simple parsers -/
+
+def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
+
+def infixR (sym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> symbol sym lbp >> termParser (lbp - 1)
+
+def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
+
+def infixL (sym : String) (lbp : Nat) : TrailingParser :=
+pushLeading >> symbol sym lbp >> termParser lbp
+
 end Parser
 
 namespace Syntax
diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index e6a502c5a2..075a3ed089 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -9,20 +9,6 @@ import Init.Lean.Parser.Level
 
 namespace Lean
 namespace Parser
-/- Helper functions for defining simple parsers -/
-
-def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
-
-def infixR (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser (lbp - 1)
-
-def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
-
-def infixL (sym : String) (lbp : Nat) : TrailingParser :=
-pushLeading >> symbol sym lbp >> termParser lbp
-
 namespace Term
 
 /- Built-in parsers -/