diff --git a/library/init/lean/ir/lirc.lean b/library/init/lean/ir/lirc.lean
index 59bc8d60cd..cc5cf30e75 100644
--- a/library/init/lean/ir/lirc.lean
+++ b/library/init/lean/ir/lirc.lean
@@ -15,9 +15,9 @@ We use it for testing.
 namespace lean
 namespace ir
 open lean.parser
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 
-def parse_input_aux : nat → list decl → fnid2string → parser (list decl × fnid2string)
+def parse_input_aux : nat → list decl → fnid2string → parsec (list decl × fnid2string)
 | 0     ds m := return (ds.reverse, m)
 | (n+1) ds m :=
   (eoi >> return (ds.reverse, m))
@@ -29,7 +29,7 @@ def parse_input_aux : nat → list decl → fnid2string → parser (list decl ×
       | none     := parse_input_aux n (d::ds) m)
 
 def parse_input (s : string) : except format (list decl × fnid2string) :=
-match parser.parse (whitespace >> parse_input_aux s.length [] mk_fnid2string) s with
+match parsec.parse (whitespace >> parse_input_aux s.length [] mk_fnid2string) s with
 | except.ok r    := return r
 | except.error m := throw (m.to_string s)
 
diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean
index 2207892cbd..4cd8692a75 100644
--- a/library/init/lean/ir/parser.lean
+++ b/library/init/lean/ir/parser.lean
@@ -4,22 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.ir.ir init.lean.parser.parser_t
+import init.lean.ir.ir init.lean.parser.parsec
 import init.lean.parser.identifier init.lean.parser.string_literal
 import init.lean.ir.reserved
 
 namespace lean
 namespace ir
 open lean.parser
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 
-def symbol (s : string) : parser unit :=
+def symbol (s : string) : parsec unit :=
 (str s >> whitespace) <?> ("'" ++ s ++ "'")
 
-def keyword (s : string) : parser unit :=
+def keyword (s : string) : parsec unit :=
 (try $ str s >> not_followed_by_sat is_id_rest >> whitespace) <?> ("'" ++ s ++ "'")
 
-def parse_type : parser type :=
+def parse_type : parsec type :=
     (keyword "bool" >> return type.bool)
 <|> (keyword "byte" >> return type.byte)
 <|> (keyword "uint16" >> return type.uint16)
@@ -33,7 +33,7 @@ def parse_type : parser type :=
 <|> (keyword "double" >> return type.double)
 <|> (keyword "object" >> return type.object)
 
-def parse_assign_unop : parser assign_unop :=
+def parse_assign_unop : parsec assign_unop :=
     (keyword "not" >> return assign_unop.not)
 <|> (keyword "neg" >> return assign_unop.neg)
 <|> (keyword "ineg" >> return assign_unop.ineg)
@@ -53,7 +53,7 @@ def parse_assign_unop : parser assign_unop :=
 <|> (keyword "tag" >> return assign_unop.tag)
 <|> (keyword "tag_ref" >> return assign_unop.tag_ref)
 
-def parse_assign_binop : parser assign_binop :=
+def parse_assign_binop : parsec assign_binop :=
     (keyword "add" >> return assign_binop.add)
 <|> (keyword "sub" >> return assign_binop.sub)
 <|> (keyword "mul" >> return assign_binop.mul)
@@ -82,7 +82,7 @@ def parse_assign_binop : parser assign_binop :=
 <|> (keyword "string_push" >> return assign_binop.string_push)
 <|> (keyword "string_append" >> return assign_binop.string_append)
 
-def parse_unop : parser unop :=
+def parse_unop : parsec unop :=
     (keyword "inc_ref" >> return unop.inc_ref)
 <|> (keyword "dec_ref" >> return unop.dec_ref)
 <|> (keyword "inc" >> return unop.inc)
@@ -93,44 +93,44 @@ def parse_unop : parser unop :=
 <|> (keyword "array_pop" >> return unop.array_pop)
 <|> (keyword "sarray_pop" >> return unop.sarray_pop)
 
-def parse_literal : parser literal :=
+def parse_literal : parsec literal :=
     (keyword "tt" >> return (literal.bool tt))
 <|> (keyword "ff" >> return (literal.bool ff))
 <|> (do n ← lexeme num <?> "numeral", return (literal.num n))
 <|> (do n ← (ch '-' >> lexeme num), return (literal.num (- n)))
 <|> literal.str <$> parse_string_literal
 
-def parse_uint16 : parser uint16 :=
+def parse_uint16 : parsec uint16 :=
 try (do p ← pos,
         n ← lexeme num,
         when (n ≥ uint16_sz) $ unexpected_at "big numeral, it does not fit in an uint16" p,
         return $ uint16.of_nat n)
 <?> "uint16"
 
-def parse_usize : parser usize :=
+def parse_usize : parsec usize :=
 try (do p ← pos,
         n ← lexeme num,
         when (n ≥ usize_sz) $ unexpected_at "big numeral, it does not fit in an usize" p,
         return $ usize.of_nat n)
 <?> "usize"
 
-def identifier : parser name :=
+def identifier : parsec name :=
 try (do p ← pos,
         n ← lean.parser.identifier,
         when (is_reserved_name n) $ unexpected_at "keyword" p,
         return n)
 <?> "identifier"
 
-def parse_var : parser var :=
+def parse_var : parsec var :=
 lexeme identifier <?> "variable"
 
-def parse_fnid : parser fnid :=
+def parse_fnid : parsec fnid :=
 lexeme identifier <?> "function name"
 
-def parse_blockid : parser blockid :=
+def parse_blockid : parsec blockid :=
 lexeme identifier <?> "label"
 
-def parse_nary_call (x : var) : parser instr :=
+def parse_nary_call (x : var) : parsec instr :=
 do xs  ← many1 parse_var,
    symbol ":=",
    keyword "call",
@@ -138,7 +138,7 @@ do xs  ← many1 parse_var,
    ys  ← many parse_var,
    return $ instr.call ([x] ++ xs) fid ys
 
-def parse_typed_assignment (x : var) : parser instr :=
+def parse_typed_assignment (x : var) : parsec instr :=
 do  symbol ":",
     ty ← parse_type,
     symbol ":=",
@@ -148,7 +148,7 @@ do  symbol ":",
 <|> (instr.assign_binop x ty <$> parse_assign_binop <*> parse_var <*> parse_var)
 <|> (instr.assign_lit x ty <$> parse_literal)
 
-def parse_untyped_assignment (x : var) : parser instr :=
+def parse_untyped_assignment (x : var) : parsec instr :=
 do  symbol ":=",
     (keyword "closure" >> instr.closure x <$> parse_fnid <*> many parse_var)
 <|> (keyword "apply"   >> instr.apply x <$> many1 parse_var)
@@ -158,13 +158,13 @@ do  symbol ":=",
 <|> (keyword "array"   >> instr.array x <$> parse_var <*> parse_var)
 <|> (keyword "sarray"  >> instr.sarray x <$> parse_type <*> parse_var <*> parse_var)
 
-def parse_assignment : parser instr :=
+def parse_assignment : parsec instr :=
 do x ← parse_var,
    c ← curr,
    if c = ':' then (parse_untyped_assignment x <|> parse_typed_assignment x)
    else parse_nary_call x
 
-def parse_instr : parser instr :=
+def parse_instr : parsec instr :=
     (keyword "array_write" >> instr.array_write <$> parse_var <*> parse_var <*> parse_var)
 <|> (keyword "set" >> instr.set <$> parse_var <*> parse_uint16 <*> parse_var)
 <|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_usize <*> parse_var)
@@ -172,27 +172,27 @@ def parse_instr : parser instr :=
 <|> (instr.unop <$> parse_unop <*> parse_var)
 <|> parse_assignment
 
-def parse_phi : parser phi :=
+def parse_phi : parsec phi :=
 do (x, ty) ← try $ do { x ← parse_var, symbol ":", ty ← parse_type, symbol ":=", keyword "phi", return (x, ty) },
    ys ← many1 parse_var,
    return {x := x, ty := ty, ys := ys}
 
-def parse_terminator : parser terminator :=
+def parse_terminator : parsec terminator :=
     (keyword "jmp" >> terminator.jmp <$> parse_blockid)
 <|> (keyword "ret" >> terminator.ret <$> many parse_var)
 <|> (keyword "case" >> terminator.case <$> parse_var <*> (symbol "[" >> sep_by1 parse_blockid (symbol ",") <* symbol "]"))
 
-def parse_block : parser block :=
+def parse_block : parsec block :=
 do id ← try (parse_blockid <* symbol ":"),
    ps ← many (parse_phi <* symbol ";"),
    is ← many (parse_instr <* symbol ";"),
    t  ← parse_terminator <* symbol ";",
    return { id := id, phis := ps, instrs := is, term := t }
 
-def parse_arg : parser arg :=
+def parse_arg : parsec arg :=
 do symbol "(", x ← parse_var, symbol ":", ty ← parse_type, symbol ")", return {n := x, ty := ty}
 
-def parse_header (is_const : bool) : parser header :=
+def parse_header (is_const : bool) : parsec header :=
 do n ← parse_fnid,
    as ← if is_const then return [] else many parse_arg,
    r ← if is_const
@@ -200,16 +200,16 @@ do n ← parse_fnid,
        else try (symbol ":" >> many1 (result.mk <$> parse_type)) <|> return [],
    return { name := n, args := as, return := r, is_const := is_const }
 
-def parse_def : parser decl :=
+def parse_def : parsec decl :=
 keyword "def" >> decl.defn <$> parse_header ff <*> (symbol ":=" >> many parse_block)
 
-def parse_defconst : parser decl :=
+def parse_defconst : parsec decl :=
 keyword "defconst" >> decl.defn <$> parse_header tt <*> (symbol ":=" >> many parse_block)
 
-def parse_external : parser decl :=
+def parse_external : parsec decl :=
 keyword "external" >> decl.external <$> parse_header ff
 
-def parse_decl : parser decl :=
+def parse_decl : parsec decl :=
 parse_def <|> parse_defconst <|> parse_external
 
 end ir
diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean
index 046bba9ed2..3231515f11 100644
--- a/library/init/lean/name_mangling.lean
+++ b/library/init/lean/name_mangling.lean
@@ -7,7 +7,7 @@ prelude
 import init.lean.name init.lean.parser.string_literal
 namespace lean
 open lean.parser
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 
 private def string.mangle_aux : nat → string.iterator → string → string
 | 0     it r := r
@@ -37,7 +37,7 @@ private def string.mangle_aux : nat → string.iterator → string → string
 def string.mangle (s : string) : string :=
 string.mangle_aux s.length s.mk_iterator ""
 
-private def parse_mangled_string_aux : nat → string → parser string
+private def parse_mangled_string_aux : nat → string → parsec string
 | 0     r := return r
 | (i+1) r :=
      (eoi >> return r)
@@ -49,11 +49,11 @@ private def parse_mangled_string_aux : nat → string → parser string
  <|> (do str "_u", d₄ ← parse_hex_digit, d₃ ← parse_hex_digit, d₂ ← parse_hex_digit, d₁ ← parse_hex_digit,
          parse_mangled_string_aux i (r.push (char.of_nat (d₄ * 4096 + d₃ * 256 + d₂ * 16 + d₁))))
 
-private def parse_mangled_string : parser string :=
+private def parse_mangled_string : parsec string :=
 do r ← remaining, parse_mangled_string_aux r ""
 
 def string.demangle (s : string) : option string :=
-(parser.parse parse_mangled_string s).to_option
+(parsec.parse parse_mangled_string s).to_option
 
 private def name.mangle_aux (pre : string) : name → string
 | name.anonymous       := pre
@@ -68,7 +68,7 @@ private def name.mangle_aux (pre : string) : name → string
 def name.mangle (n : name) (pre : string := "_l") : string :=
 name.mangle_aux pre n
 
-private def parse_mangled_name_aux : nat → name → parser name
+private def parse_mangled_name_aux : nat → name → parsec name
 | 0 r     := return r
 | (i+1) r :=
       (eoi >> return r)
@@ -78,10 +78,10 @@ private def parse_mangled_name_aux : nat → name → parser name
   <|> (do ch '_', n ← num, ch '_',
           parse_mangled_name_aux i (r.mk_numeral n))
 
-private def parse_mangled_name (pre : string) : parser name :=
+private def parse_mangled_name (pre : string) : parsec name :=
 do str pre, r ← remaining, parse_mangled_name_aux r name.anonymous
 
 def name.demangle (s : string) (pre : string := "_l") : option name :=
-(parser.parse (parse_mangled_name pre) s).to_option
+(parsec.parse (parse_mangled_name pre) s).to_option
 
 end lean
diff --git a/library/init/lean/parser/identifier.lean b/library/init/lean/parser/identifier.lean
index 46d11528f6..7f0da4d863 100644
--- a/library/init/lean/parser/identifier.lean
+++ b/library/init/lean/parser/identifier.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.char.basic init.lean.parser.parser_t
+import init.data.char.basic init.lean.parser.parsec
 
 namespace lean
 
@@ -38,8 +38,8 @@ def is_id_end_escape (c : char) : bool :=
 c = id_end_escape
 
 namespace parser
-variables {m : Type → Type} [monad m] [monad_parser m] [alternative m]
-open monad_parser
+variables {m : Type → Type} [monad m] [monad_parsec m] [alternative m]
+open monad_parsec
 
 def id_part_default : m string :=
 do c ← satisfy is_id_first,
diff --git a/library/init/lean/parser/parser_t.lean b/library/init/lean/parser/parsec.lean
similarity index 89%
rename from library/init/lean/parser/parser_t.lean
rename to library/init/lean/parser/parsec.lean
index 85614c97f7..96c7ed6566 100644
--- a/library/init/lean/parser/parser_t.lean
+++ b/library/init/lean/parser/parsec.lean
@@ -55,26 +55,26 @@ inductive result (α : Type)
 @[inline] def result.mk_eps {α : Type} (a : α) (it : iterator) : result α :=
 result.ok_eps a it dlist.empty
 
-def parser (α : Type) :=
+def parsec (α : Type) :=
 iterator → result α
 
-namespace parser
+namespace parsec
 open result
 variables {α β : Type}
 
-def run (p : parser α) (s : string) (fname := "") : except message α :=
+def run (p : parsec α) (s : string) (fname := "") : except message α :=
 match p s.mk_iterator with
 | ok a _       := except.ok a
 | ok_eps a _ _ := except.ok a
 | error msg _  := except.error msg
 
-protected def pure (a : α) : parser α :=
+protected def pure (a : α) : parsec α :=
 λ it, mk_eps a it
 
-def eps : parser unit :=
-parser.pure ()
+def eps : parsec unit :=
+parsec.pure ()
 
-protected def failure : parser α :=
+protected def failure : parsec α :=
 λ it, error { unexpected := "failure", pos := it.offset } ff
 
 def merge (msg₁ msg₂ : message) : message :=
@@ -87,7 +87,7 @@ def merge (msg₁ msg₂ : message) : message :=
   3- If `q` succeeds but does not consume input, then execute `q`
      and merge error messages if both do not consume any input.
 -/
-protected def bind (p : parser α) (q : α → parser β) : parser β :=
+protected def bind (p : parsec α) (q : α → parsec β) : parsec β :=
 λ it, match p it with
      | ok a it :=
        (match q a it with
@@ -101,16 +101,16 @@ protected def bind (p : parser α) (q : α → parser β) : parser β :=
         | other           := other)
      | error msg c := error msg c
 
-instance : monad parser :=
-{ bind := @parser.bind, pure := @parser.pure }
+instance : monad parsec :=
+{ bind := @parsec.bind, pure := @parsec.pure }
 
-instance : monad_fail parser :=
+instance : monad_fail parsec :=
 { fail := λ _ s it, error { unexpected := s, pos := it.offset } ff }
 
 def expect (msg : message) (exp : string) : message :=
 {expected := dlist.singleton exp, ..msg}
 
-@[inline] def label (p : parser α) (ex : string) : parser α :=
+@[inline] def label (p : parsec α) (ex : string) : parsec α :=
 λ it, match p it with
       | ok_eps a it _  := ok_eps a it (dlist.singleton ex)
       | error msg ff   := error (expect msg ex) ff
@@ -133,7 +133,7 @@ together.
 ```
 Without the `try` combinator we will not be able to backtrack on the `let` keyword.
 -/
-def try (p : parser α) : parser α :=
+def try (p : parsec α) : parsec α :=
 λ it, match p it with
       | error msg _  := error msg ff
       | other        := other
@@ -153,7 +153,7 @@ def try (p : parser α) : parser α :=
      it combines their error messages (even if one of
      them succeeded).
 -/
-protected def orelse (p q : parser α) : parser α :=
+protected def orelse (p q : parsec α) : parsec α :=
 λ it, match p it with
       | ok_eps a it' ex₁ :=
         (match q it with
@@ -167,42 +167,42 @@ protected def orelse (p q : parser α) : parser α :=
          | other            := other)
       | other              := other
 
-instance : alternative parser :=
-{ orelse  := @parser.orelse,
-  failure := @parser.failure }
+instance : alternative parsec :=
+{ orelse  := @parsec.orelse,
+  failure := @parsec.failure }
 
 /-- Parse `p` without consuming any input. -/
-def lookahead (p : parser α) : parser α :=
+def lookahead (p : parsec α) : parsec α :=
 λ it, match p it with
       | ok a s' := mk_eps a it
       | other   := other
 
 /-- `not_followed_by p` succeeds when parser `p` fails -/
-def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
+def not_followed_by (p : parsec α) (msg : string := "input") : parsec unit :=
 λ it, match p it with
       | ok _ _       := error { pos := it.offset, unexpected := msg } ff
       | ok_eps _ _ _ := error { pos := it.offset, unexpected := msg } ff
       | error _ _    := mk_eps () it
-end parser
+end parsec
 
-/- Type class for abstracting from concrete monad stacks containing a `parser_t` somewhere. -/
-class monad_parser (m : Type → Type) :=
+/- Type class for abstracting from concrete monad stacks containing a `parsec` somewhere. -/
+class monad_parsec (m : Type → Type) :=
 -- analogous to e.g. `monad_state.lift`
-(lift {} {α : Type} : parser α → m α)
+(lift {} {α : Type} : parsec α → m α)
 -- Analogous to e.g. `monad_reader_adapter.map` before simplification (see there).
 -- Its usage seems to be way too common to justify moving it into a separate type class.
-(map {} {α : Type} : (∀ {α}, parser α → parser α) → m α → m α)
+(map {} {α : Type} : (∀ {α}, parsec α → parsec α) → m α → m α)
 
-instance {m : Type → Type} [monad m] : monad_parser parser :=
+instance {m : Type → Type} [monad m] : monad_parsec parsec :=
 { lift := λ α p, p,
   map  := λ α f x, f x }
 
-instance monad_parser_trans {m n : Type → Type} [has_monad_lift m n] [monad_functor m m n n] [monad_parser m] : monad_parser n :=
-{ lift := λ α p, monad_lift (monad_parser.lift p : m α),
-  map  := λ α f x, monad_map (λ β x, (monad_parser.map @f x : m β)) x }
+instance monad_parsec_trans {m n : Type → Type} [has_monad_lift m n] [monad_functor m m n n] [monad_parsec m] : monad_parsec n :=
+{ lift := λ α p, monad_lift (monad_parsec.lift p : m α),
+  map  := λ α f x, monad_map (λ β x, (monad_parsec.map @f x : m β)) x }
 
-namespace monad_parser
-variables {m : Type → Type} [monad m] [monad_parser m] [alternative m] {α β : Type}
+namespace monad_parsec
+variables {m : Type → Type} [monad m] [monad_parsec m] [alternative m] {α β : Type}
 
 @[inline] def error {α : Type} (unexpected : string := "") (expected : dlist string := dlist.empty) : m α :=
 lift $ λ it, result.error ⟨it.offset, unexpected, expected⟩ ff
@@ -211,7 +211,7 @@ def left_over : m iterator :=
 lift $ λ it, result.mk_eps it it
 
 @[inline] def label (p : m α) (ex : string) : m α :=
-map (λ _ p, @parser.label _ p ex) p
+map (λ _ p, @parsec.label _ p ex) p
 
 infixr ` <?> `:2 := label
 
@@ -233,17 +233,17 @@ together.
 Without the `try` combinator we will not be able to backtrack on the `let` keyword.
 -/
 @[inline] def try (p : m α) : m α :=
-map (λ _ p, parser.try p) p
+map (λ _ p, parsec.try p) p
 
 /-- Parse `p` without consuming any input. -/
 @[inline] def lookahead (p : m α) : m α :=
-map (λ _ p, parser.lookahead p) p
+map (λ _ p, parsec.lookahead p) p
 
 -- TODO(Sebastian): `monad_functor` is too weak to lift this, probably needs something like `monad_control`
 /-
 /-- `not_followed_by p` succeeds when parser `p` fails -/
 @[inline] def not_followed_by (p : m α) (msg : string := "input") : m unit :=
-map (λ _ _ inst p, @parser_t.not_followed_by _ inst _ p msg) p
+map (λ _ _ inst p, @parsec_t.not_followed_by _ inst _ p msg) p
 -/
 
 /-- Faster version of `not_followed_by (satisfy p)` -/
@@ -480,21 +480,21 @@ error msg
 def unexpected_at (msg : string) (pos : position) : m α :=
 lift $ λ _, result.error {unexpected := msg, pos := pos} ff
 
-end monad_parser
+end monad_parsec
 
-namespace parser
-open monad_parser
+namespace parsec
+open monad_parsec
 variables {m : Type → Type} [monad m] {α β : Type}
 
-def parse (p : parser α) (s : string) (fname := "") : except message α :=
+def parse (p : parsec α) (s : string) (fname := "") : except message α :=
 run p s fname
 
-def parse_with_eoi (p : parser α) (s : string) (fname := "") : except message α :=
+def parse_with_eoi (p : parsec α) (s : string) (fname := "") : except message α :=
 run (p <* eoi) s fname
 
-def parse_with_left_over (p : parser α) (s : string) (fname := "") : except message (α × iterator) :=
+def parse_with_left_over (p : parsec α) (s : string) (fname := "") : except message (α × iterator) :=
 run (prod.mk <$> p <*> left_over) s fname
 
-end parser
+end parsec
 end parser
 end lean
diff --git a/library/init/lean/parser/reader/basic.lean b/library/init/lean/parser/reader/basic.lean
index 58fa0d668b..4737406360 100644
--- a/library/init/lean/parser/reader/basic.lean
+++ b/library/init/lean/parser/reader/basic.lean
@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Reader for the Lean language
 -/
 prelude
-import init.lean.parser.parser_t init.lean.parser.syntax init.lean.parser.macro
+import init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.macro
 import init.lean.parser.identifier
 
 namespace lean
@@ -22,7 +22,7 @@ structure token_config :=
    It should return a syntax tree with a "hole" for the
    `source_info` surrounding the token, which will be supplied
    by the `token` reader. -/
-(token_reader : option (parser (source_info → syntax)) := none)
+(token_reader : option (parsec (source_info → syntax)) := none)
 
 structure reader_state :=
 (tokens : list token_config)
@@ -34,7 +34,7 @@ def reader_state.empty : reader_state :=
 
 structure reader_config := mk
 
-@[irreducible] def read_m := reader_t reader_config $ state_t reader_state $ parser
+@[irreducible] def read_m := reader_t reader_config $ state_t reader_state $ parsec
 
 structure reader :=
 (read : read_m syntax)
@@ -46,7 +46,7 @@ instance : monad read_m := infer_instance
 instance : alternative read_m := infer_instance
 instance : monad_reader reader_config read_m := infer_instance
 instance : monad_state reader_state read_m := infer_instance
-instance : monad_parser read_m := infer_instance
+instance : monad_parsec read_m := infer_instance
 
 --TODO(Sebastian): expose `reader_state.errors`
 protected def run {α : Type} (cfg : reader_config) (st : reader_state) (s : string) (r : read_m α) :
@@ -55,7 +55,7 @@ prod.fst <$> ((r.run cfg).run st).parse_with_eoi s
 end read_m
 
 namespace reader
-open monad_parser
+open monad_parsec
 
 protected def parse (cfg : reader_config) (s : string) (r : reader) :
   except parser.message syntax :=
diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean
index 37efe2d1bf..0dcfadf612 100644
--- a/library/init/lean/parser/reader/module.lean
+++ b/library/init/lean/parser/reader/module.lean
@@ -10,7 +10,7 @@ import init.lean.parser.reader.token
 
 namespace lean.parser
 namespace reader
-open monad_parser
+open monad_parsec
 
 def «prelude» := {macro . name := `prelude}
 
diff --git a/library/init/lean/parser/reader/token.lean b/library/init/lean/parser/reader/token.lean
index 013de518a4..1e7064cd71 100644
--- a/library/init/lean/parser/reader/token.lean
+++ b/library/init/lean/parser/reader/token.lean
@@ -17,7 +17,7 @@ import init.lean.parser.reader.basic init.util
 
 namespace lean.parser
 namespace reader
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 open string
 
 def match_token : read_m (option token_config) :=
@@ -95,7 +95,7 @@ do (r, i) ← with_source_info $ do {
        do str tk,
           pure $ λ i, syntax.atom ⟨some i, atomic_val.string tk⟩
      -- variable-length token
-     | some ⟨tk, some r⟩ := str tk *> monad_parser.lift r
+     | some ⟨tk, some r⟩ := str tk *> monad_parsec.lift r
      | none              := number' <|> ident'
    },
    pure (r i)
diff --git a/library/init/lean/parser/string_literal.lean b/library/init/lean/parser/string_literal.lean
index 09511e1419..67d60c2f65 100644
--- a/library/init/lean/parser/string_literal.lean
+++ b/library/init/lean/parser/string_literal.lean
@@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.parser.parser_t
+import init.lean.parser.parsec
 
 namespace lean
 namespace parser
-open monad_parser
+open monad_parsec
 
-def parse_hex_digit : parser nat :=
+def parse_hex_digit : parsec nat :=
 (    (do d ← digit, return $ d.val - '0'.val)
  <|> (do c ← satisfy (λ c, 'a'.val ≤ c.val && c.val ≤ 'f'.val), return $ 10 + (c.val - 'a'.val))
  <|> (do c ← satisfy (λ c, 'A'.val ≤ c.val && c.val ≤ 'F'.val), return $ 10 + (c.val - 'A'.val)))
 <?> "hexadecimal"
 
-def parse_quoted_char : parser char :=
+def parse_quoted_char : parsec char :=
 do p ← pos,
    c ← any,
    if c = '\\'      then return '\\'
@@ -36,7 +36,7 @@ do p ← pos,
      return $ char.of_nat (16*(16*(16*d₁ + d₂) + d₃) + d₄) }
    else unexpected_at "quoted character" p
 
-def parse_string_literal_aux : nat → string → parser string
+def parse_string_literal_aux : nat → string → parsec string
 | 0     s := ch '\"' >> return s
 | (n+1) s := do
   c ← any,
@@ -44,7 +44,7 @@ def parse_string_literal_aux : nat → string → parser string
   else if c = '\"' then return s
   else parse_string_literal_aux n (s.push c)
 
-def parse_string_literal : parser string :=
+def parse_string_literal : parsec string :=
 do ch '\"',
    r ← remaining,
    parse_string_literal_aux r ""
diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
index f7fee98535..6ea558de76 100644
--- a/library/init/lean/parser/syntax.lean
+++ b/library/init/lean/parser/syntax.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich
 -/
 prelude
-import init.lean.name init.lean.parser.parser_t
+import init.lean.name init.lean.parser.parsec
 
 namespace lean
 namespace parser
diff --git a/tests/lean/parser1.lean b/tests/lean/parsec1.lean
similarity index 90%
rename from tests/lean/parser1.lean
rename to tests/lean/parsec1.lean
index 091fa69478..600b902888 100644
--- a/tests/lean/parser1.lean
+++ b/tests/lean/parsec1.lean
@@ -1,19 +1,19 @@
 import system.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format
 open lean.parser
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 
-def test {α} [decidable_eq α] (p : parser α) (s : string) (e : α) : io unit :=
-match parser.parse p s with
+def test {α} [decidable_eq α] (p : parsec α) (s : string) (e : α) : io unit :=
+match parsec.parse p s with
 | except.ok a    := if a = e then return () else io.print_ln "unexpected result"
 | except.error e := io.print_ln (e.to_string s)
 
-def test_failure {α} (p : parser α) (s : string) : io unit :=
-match parser.parse p s with
+def test_failure {α} (p : parsec α) (s : string) : io unit :=
+match parsec.parse p s with
 | except.ok a    := io.print_ln "unexpected success"
 | except.error e := return ()
 
-def show_result {α} [has_to_string α] (p : parser α) (s : string) : io unit :=
-match parser.parse p s with
+def show_result {α} [has_to_string α] (p : parsec α) (s : string) : io unit :=
+match parsec.parse p s with
 | except.ok a    := io.print_ln "result: " >> io.print_ln (repr $ to_string a)
 | except.error e := io.print_ln (e.to_string s)
 
@@ -37,12 +37,12 @@ match parser.parse p s with
 #eval test (str "ab" >> pure () <|> (ch 'a' >> ch 'c' >> pure ())) "ac" ()
 #eval test (try (ch 'a' >> ch 'b') <|> (ch 'a' >> ch 'c')) "ac" 'c'
 #eval test (lookahead (ch 'a')) "abc" 'a'
-#eval test_failure (parser.not_followed_by (lookahead (ch 'a'))) "abc"
+#eval test_failure (parsec.not_followed_by (lookahead (ch 'a'))) "abc"
 
-def symbol (c : char) : parser char :=
+def symbol (c : char) : parsec char :=
 lexeme (ch c) <?> repr c
 
-def paren {α} (p : parser α) : parser α :=
+def paren {α} (p : parsec α) : parsec α :=
 symbol '(' >> lexeme p <* symbol ')'
 
 #eval test (paren num) "(   10 )" 10
@@ -50,7 +50,7 @@ symbol '(' >> lexeme p <* symbol ')'
 #eval test (paren num) "(0)" 0
 #eval test (paren num) "(0    )" 0
 
-def var : parser string :=
+def var : parsec string :=
 do c ← satisfy (λ a, a.is_alpha || a = '_'),
    r ← lexeme $ take_while (λ a, a.is_digit || a.is_alpha || a = '_'),
    return (c.to_string ++ r)
@@ -96,7 +96,7 @@ open lean
 #eval test_failure parse_string_literal "\"\\u03b\\u03b1\""
 #eval test_failure parse_string_literal "\"\\u03bz\\u03b1\""
 
-def parse_instr_pp : parser string :=
+def parse_instr_pp : parsec string :=
 do cmd ← lean.ir.parse_instr,
    return $ to_string cmd
 
@@ -151,18 +151,18 @@ instance eq_expr : decidable_eq Expr
                     | is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h')))
   | is_false h := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₁ h))
 
-def parse_atom (p : parser Expr) : parser Expr :=
+def parse_atom (p : parsec Expr) : parsec Expr :=
 (Var <$> lexeme var <?> "variable")
 <|>
 (Num <$> lexeme num <?> "numeral")
 <|>
 (paren p)
 
-def parse_add (p : parser Expr) : parser Expr :=
+def parse_add (p : parsec Expr) : parsec Expr :=
 do l ← parse_atom p,
    (do symbol '+', r ← p, return $ Add l r) <|> return l
 
-def parse_expr : parser Expr :=
+def parse_expr : parsec Expr :=
 whitespace >> fix (λ F, parse_add F) <* eoi
 
 #eval test parse_expr "10" (Num 10)
@@ -181,9 +181,9 @@ whitespace >> fix (λ F, parse_add F) <* eoi
 
 namespace paper_ex
 #print "Failure 3"
-def digit  : parser char := monad_parser.digit <?> "digit"
-def letter : parser char := monad_parser.alpha <?> "letter"
-def tst    : parser char := (digit <|> return '0') >> letter
+def digit  : parsec char := monad_parsec.digit <?> "digit"
+def letter : parsec char := monad_parsec.alpha <?> "letter"
+def tst    : parsec char := (digit <|> return '0') >> letter
 #eval test tst "*" 'a'
 #print "---------"
 end paper_ex
diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parsec1.lean.expected.out
similarity index 100%
rename from tests/lean/parser1.lean.expected.out
rename to tests/lean/parsec1.lean.expected.out
diff --git a/tests/lean/run/display_hw_term_hack_deps.lean b/tests/lean/run/display_hw_term_hack_deps.lean
index 117f6da51a..b4bdd77ce7 100644
--- a/tests/lean/run/display_hw_term_hack_deps.lean
+++ b/tests/lean/run/display_hw_term_hack_deps.lean
@@ -1,5 +1,5 @@
 import init.lean.parser.syntax
-import init.lean.parser.parser_t
+import init.lean.parser.parsec
 import init.lean.ir.type_check init.lean.ir.ssa_check init.lean.ir.elim_phi init.lean.ir.parser
 
 open tactic
diff --git a/tests/lean/run/name_mangling.lean b/tests/lean/run/name_mangling.lean
index f483af9c39..4d1da11da8 100644
--- a/tests/lean/run/name_mangling.lean
+++ b/tests/lean/run/name_mangling.lean
@@ -3,7 +3,7 @@ open lean lean.parser
 open tactic
 
 meta def check (s : string) : tactic unit :=
-match id.run $ parser.parse identifier s with
+match id.run $ parsec.parse identifier s with
 | except.ok n     :=
   trace (name.mangle n) >>
   if name.demangle (name.mangle n) = some n then exact `(true)
diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean
index 1c7cc191a0..cdaca67b8e 100644
--- a/tests/lean/run/parser_ir1.lean
+++ b/tests/lean/run/parser_ir1.lean
@@ -4,7 +4,7 @@ import init.lean.ir.elim_phi init.lean.ir.type_check
 import init.lean.ir.extract_cpp
 
 open lean.parser
-open lean.parser.monad_parser
+open lean.parser.monad_parsec
 open lean.ir
 
 def check_decl (d : decl) : io unit :=
@@ -12,8 +12,8 @@ match type_check d with
 | except.ok _    := return ()
 | except.error e := io.print_ln (to_string e)
 
-def show_result (p : parser decl) (s : string) : io unit :=
-match parser.parse p s with
+def show_result (p : parsec decl) (s : string) : io unit :=
+match parsec.parse p s with
 | except.ok d    := io.print_ln (lean.to_fmt d) >> check_decl d
 | except.error e := io.print_ln (e.to_string s)
 
@@ -45,7 +45,7 @@ end:
 #eval show_result (whitespace >> parse_def) IR2
 
 def tst_elim_phi (s : string) : io unit :=
-do (except.ok d) ← return $ parser.parse (whitespace >> parse_def) s,
+do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s,
    check_decl d,
    io.print_ln (lean.to_fmt (elim_phi d))
 
@@ -66,7 +66,7 @@ main:
 #eval show_result (whitespace >> parse_def) IR3
 
 def tst_extract_cpp (s : string) : io unit :=
-do (except.ok d) ← return $ parser.parse (whitespace >> parse_def) s,
+do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s,
    check_decl d,
    match extract_cpp [elim_phi d] with
    | except.ok code := io.print_ln code