diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean
index 6f791686f5..4b9f0ab40a 100644
--- a/library/init/lean/parser/parsec.lean
+++ b/library/init/lean/parser/parsec.lean
@@ -362,11 +362,14 @@ This parser consumes no input if it fails (even if a partial match).
 Note: The behaviour of this parser is different to that the `string` parser in the Parsec_t Μ M Haskell library,
 as this one is all-or-nothing.
 -/
-def str (s : string) : m string :=
+def str_core (s : string) (ex : dlist string) : m string :=
 if s.is_empty then pure ""
 else lift $ λ it, match str_aux s.length s.mk_iterator it with
   | some it' := result.ok s it' none
-  | none     := result.error { it := it, expected := dlist.singleton (repr s), custom := none } ff
+  | none     := result.error { it := it, expected := ex, custom := none } ff
+
+@[inline] def str (s : string) : m string :=
+str_core s (dlist.singleton (repr s))
 
 private def take_aux : nat → string → iterator → result μ string
 | 0     r it := result.ok r it none
diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean
index 6e3cb38737..3f842c5ea2 100644
--- a/library/init/lean/parser/token.lean
+++ b/library/init/lean/parser/token.lean
@@ -107,7 +107,7 @@ instance raw.view {α} (p : m α) (t) : parser.has_view (option syntax_atom) (ra
   review := λ a, (syntax.atom <$> a).get_or_else syntax.missing }
 
 /-- Like `raw (str s)`, but default to `s` in views. -/
-@[derive has_tokens has_view]
+@[inline, derive has_tokens has_view]
 def raw_str (s : string) (trailing_ws := ff) : parser :=
 raw (str s) trailing_ws