diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 14d9750f35..8694c4ded6 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -34,10 +34,10 @@ instance coe_name_ident : has_coe name parser.ident.view :=
       suffix := suffix <&> λ suffix, {ident := review parser.ident suffix}}
   | _ := some $ view parser.ident syntax.missing) none).get_or_else (view parser.ident syntax.missing)⟩
 
-instance coe_ident_term_ident : has_coe parser.ident.view term.ident.view :=
+instance coe_ident_ident_univs : has_coe parser.ident.view ident_univs.view :=
 ⟨λ id, {id := id}⟩
 
-instance coe_term_ident_binder_id : has_coe term.ident.view binder_ident.view :=
+instance coe_ident_binder_id : has_coe ident.view binder_ident.view :=
 ⟨binder_ident.view.id⟩
 
 instance coe_binders {α : Type} [has_coe_t α binder_ident.view] : has_coe (list α) term.binders.view :=
@@ -94,12 +94,12 @@ def mixfix.transform : transformer :=
   let term := match v.kind with
   | mixfix.kind.view.prefix _ :=
     -- `prefix tk:prec? := e` ~> `notation tk:prec? b:prec? := e b`
-    review app {fn := v.term, arg := review term.ident `b}
+    review app {fn := v.term, arg := review ident_univs `b}
   | mixfix.kind.view.postfix _ :=
     -- `postfix tk:prec? := e` ~> `notation tk:prec? b:prec? := e b`
-    review app {fn := v.term, arg := review term.ident `a}
+    review app {fn := v.term, arg := review ident_univs `a}
   | _ :=
-    review app {fn := review app {fn := v.term, arg := review term.ident `a}, arg := review term.ident `b},
+    review app {fn := review app {fn := v.term, arg := review ident_univs `a}, arg := review ident_univs `b},
   pure $ review «notation» {«local» := v.local, spec := spec, term := term}
 
 def reserve_mixfix.transform : transformer :=
diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean
index 72def3325f..d38f14423c 100644
--- a/library/init/lean/parser/declaration.lean
+++ b/library/init/lean/parser/declaration.lean
@@ -105,7 +105,7 @@ def structure.parser : command_parser :=
 node! «structure» [
   keyword: any_of [symbol "structure", symbol "class"],
   old_univ_params: old_univ_params.parser?,
-  name: term.ident.parser,
+  name: ident_univs.parser,
   sig: decl_sig.parser,
   «extends»: node! «extends» ["extends", parents: sep_by1 term.parser (symbol ",")]?,
   ":=",
@@ -121,15 +121,15 @@ node! declaration [
     «def_like»: node! «def_like» [
       kind: node_choice! def_like.kind {"def", "abbreviation", "theorem"},
       old_univ_params: old_univ_params.parser?,
-      name: term.ident.parser, sig: decl_sig.parser, val: decl_val.parser],
-    «instance»: node! «instance» ["instance", name: term.ident.parser?, sig: decl_sig.parser, val: decl_val.parser],
+      name: ident_univs.parser, sig: decl_sig.parser, val: decl_val.parser],
+    «instance»: node! «instance» ["instance", name: ident_univs.parser?, sig: decl_sig.parser, val: decl_val.parser],
     «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser],
-    «constant»: node! «constant» ["constant", name: term.ident.parser, sig: decl_sig.parser],
-    «axiom»: node! «axiom» ["axiom", name: term.ident.parser, sig: decl_sig.parser],
+    «constant»: node! «constant» ["constant", name: ident_univs.parser, sig: decl_sig.parser],
+    «axiom»: node! «axiom» ["axiom", name: ident_univs.parser, sig: decl_sig.parser],
 
     «inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"],
       old_univ_params: old_univ_params.parser?,
-      name: term.ident.parser,
+      name: ident_univs.parser,
       sig: decl_sig.parser,
       local_notation: notation_like.parser?,
       intro_rules: intro_rule.parser*],
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 59904e9c99..9c4102fd3c 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -23,8 +23,8 @@ def ident_univ_spec.parser : basic_parser :=
 node! ident_univ_spec [".{", levels: level.parser+, "}"]
 
 @[derive parser.has_tokens parser.has_view]
-protected def term.ident.parser : term_parser :=
-node! term.ident [id: ident.parser, univ: (monad_lift ident_univ_spec.parser)?]
+def ident_univs.parser : term_parser :=
+node! ident_univs [id: ident.parser, univ: (monad_lift ident_univ_spec.parser)?]
 
 namespace term
 /-- Access leading term -/
@@ -177,7 +177,7 @@ node! explicit [
     explicit: symbol "@" max_prec,
     partial_explicit: symbol "@@" max_prec
   },
-  id: term.ident.parser
+  id: ident_univs.parser
 ]
 
 @[derive parser.has_tokens parser.has_view]
@@ -290,7 +290,7 @@ node! anonymous_inaccessible ["._":max_prec]
 -- TODO(Sebastian): replace with attribute
 @[derive has_tokens]
 def builtin_leading_parsers : list term_parser := [
-  term.ident.parser,
+  ident_univs.parser,
   number.parser,
   paren.parser,
   hole.parser,
diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out
index 1c0a151d62..9ef7ba5ecb 100644
--- a/tests/lean/parser1.lean.expected.out
+++ b/tests/lean/parser1.lean.expected.out
@@ -93,8 +93,8 @@ result:
   (term.app
    (term.app
     (term.sort_app (term.sort (1 "Type")) (level.leading (0 `max)))
-    (term.ident `u []))
-   (term.ident `v [])))
+    (ident_univs `u []))
+   (ident_univs `v [])))
  (eoi "")]
 (ok (some "notationa`+`:65 b:65 :=nat.addab"))
 parser1.lean:132:0: warning: using 'exit' to interrupt Lean