diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 73a2d510d0..36d6edd4fe 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -34,7 +34,7 @@ builtin_initialize
 def notFollowedByRedefinedTermToken :=
   -- Remark: we don't currently support `open` and `set_option` in `do`-blocks, but we include them in the following list to fix the ambiguity
   -- "open" command following `do`-block. If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
-  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
+  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
 
 @[builtinDoElemParser] def doLet      := leading_parser "let " >> optional "mut " >> letDecl
 
@@ -105,7 +105,7 @@ def doFinally    := leading_parser "finally " >> doSeq
 @[builtinDoElemParser] def doBreak     := leading_parser "break"
 @[builtinDoElemParser] def doContinue  := leading_parser "continue"
 @[builtinDoElemParser] def doReturn    := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
-@[builtinDoElemParser] def doDbgTrace  := leading_parser:leadPrec "dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)
+@[builtinDoElemParser] def doDbgTrace  := leading_parser:leadPrec (symbol "dbgTrace! " <|> "dbg_trace ") >> ((interpolatedStr termParser) <|> termParser)
 @[builtinDoElemParser] def doAssert    := leading_parser:leadPrec "assert! " >> termParser
 
 /-
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2108571a19..11d4ca73a9 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -182,15 +182,15 @@ def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> o
 @[runBuiltinParserAttributeHooks]
 def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 
-@[builtinTermParser] def noindex := leading_parser "noindex!" >> termParser maxPrec
+@[builtinTermParser] def noindex := leading_parser (symbol "noindex! " <|> "no_index ") >> termParser maxPrec
 
-@[builtinTermParser] def binrel  := leading_parser "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
+@[builtinTermParser] def binrel  := leading_parser (symbol "binrel! " <|> "binrel%") >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
 
-@[builtinTermParser] def forInMacro := leading_parser "forIn! " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
+@[builtinTermParser] def forInMacro := leading_parser (symbol "forIn! " <|> "forIn% ") >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
 
-@[builtinTermParser] def typeOf             := leading_parser "typeOf! " >> termParser maxPrec
-@[builtinTermParser] def ensureTypeOf       := leading_parser "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
-@[builtinTermParser] def ensureExpectedType := leading_parser "ensureExpectedType! " >> strLit >> termParser maxPrec
+@[builtinTermParser] def typeOf             := leading_parser (symbol "typeOf! " <|> "typeOf% ") >> termParser maxPrec
+@[builtinTermParser] def ensureTypeOf       := leading_parser (symbol "ensureTypeOf! " <|> "ensureTypeOf% ") >> termParser maxPrec >> strLit >> termParser
+@[builtinTermParser] def ensureExpectedType := leading_parser (symbol "ensureExpectedType! " <|> "ensureExpectedType% ") >> strLit >> termParser maxPrec
 
 def namedArgument  := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := leading_parser ".."
@@ -223,7 +223,7 @@ def bracketedBinderF := bracketedBinder  -- no default arg
 
 @[builtinTermParser] def panic       := leading_parser:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
-@[builtinTermParser] def dbgTrace    := leading_parser:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
+@[builtinTermParser] def dbgTrace    := leading_parser:leadPrec withPosition ((symbol "dbgTrace! " <|> "dbg_trace") >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
 @[builtinTermParser] def assert      := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser