diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 9416d4e862..7067835be1 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -17,16 +17,9 @@ builtin_initialize
   registerBuiltinParserAttribute `builtinPrecParser `prec (leadingIdentAsSymbol := true)
   registerBuiltinDynamicParserAttribute `precParser `prec
 
-builtin_initialize
-  registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true)
-  registerBuiltinDynamicParserAttribute `prioParser `prio
-
 @[inline] def precedenceParser (rbp : Nat := 0) : Parser :=
   categoryParser `prec rbp
 
-@[inline] def priorityParser (rbp : Nat := 0) : Parser :=
-  categoryParser `prio rbp
-
 @[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
   categoryParser `stx rbp
 
@@ -36,9 +29,6 @@ def optPrecedence := optional (atomic «precedence»)
 namespace Syntax
 @[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit
 
-@[builtinPrioParser] def numPrio  := checkPrec maxPrec >> numLit
-@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high"
-
 @[builtinSyntaxParser] def paren           := parser! "(" >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def cat             := parser! ident >> optPrecedence
 @[builtinSyntaxParser] def unary           := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
@@ -58,10 +48,6 @@ namespace Term
 
 end Term
 
-namespace AttrParam
-@[builtinAttrParamParser] def prio  := parser!:maxPrec "priority: " >> priorityParser maxPrec
-end AttrParam
-
 namespace Command
 
 def optPrio   := optional ("[" >> priorityParser >> "]")
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2672c0ba86..54ecad873c 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -13,6 +13,10 @@ builtin_initialize
   registerBuiltinParserAttribute `builtinTacticParser `tactic (leadingIdentAsSymbol := true)
   registerBuiltinDynamicParserAttribute `tacticParser `tactic
 
+builtin_initialize
+  registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true)
+  registerBuiltinDynamicParserAttribute `prioParser `prio
+
 builtin_initialize
   registerBuiltinParserAttribute `builtinAttrParamParser `attrParam (leadingIdentAsSymbol := true)
   registerBuiltinDynamicParserAttribute `attrParamParser `attrParam
@@ -20,6 +24,9 @@ builtin_initialize
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
   categoryParser `tactic rbp
 
+@[inline] def priorityParser (rbp : Nat := 0) : Parser :=
+  categoryParser `prio rbp
+
 @[inline] def attrParamParser (rbp : Nat := 0) : Parser :=
   categoryParser `attrParam rbp
 
@@ -40,10 +47,16 @@ end Tactic
 
 def darrow : Parser := " => "
 
+namespace Priority
+@[builtinPrioParser] def numPrio  := checkPrec maxPrec >> numLit
+@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high"
+end Priority
+
 namespace AttrParam
 @[builtinAttrParamParser] def ident := checkPrec maxPrec >> Parser.ident
 @[builtinAttrParamParser] def str   := checkPrec maxPrec >> strLit
 @[builtinAttrParamParser] def num   := checkPrec maxPrec >> numLit
+@[builtinAttrParamParser] def prio  := parser!:maxPrec "priority: " >> priorityParser maxPrec
 end AttrParam
 
 namespace Term