diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean
index 1e0d4b2ddc..b707a2607a 100644
--- a/library/data/buffer/parser.lean
+++ b/library/data/buffer/parser.lean
@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import data.buffer data.dlist
-universes u v
 
-inductive parse_result (α : Type u)
+inductive parse_result (α : Type)
 | done (pos : ℕ) (result : α) : parse_result
 | fail (pos : ℕ) (expected : dlist string) : parse_result
 
-def parser (α : Type u) :=
+def parser (α : Type) :=
 ∀ (input : char_buffer) (start : ℕ), parse_result α
 
 namespace parser
--- Type polymorphism is restricted here because of monad.bind
 variables {α β γ : Type}
 
 protected def bind (p : parser α) (f : α → parser β) : parser β :=
@@ -51,7 +49,7 @@ protected def fail (msg : string) : parser α :=
 instance : monad parser :=
 { pure := @parser.pure, bind := @parser.bind }
 
-instance : is_lawful_monad parser.{0} :=
+instance : is_lawful_monad parser :=
 { id_map := @parser.id_map,
   pure_bind := λ _ _ _ _, rfl,
   bind_assoc := @parser.bind_assoc }