diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 7d3fb4098e..0060cc0bcd 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -359,7 +359,7 @@ syntax (name := delta) "delta " ident (location)? : tactic
 
 -- Auxiliary macro for lifting have/suffices/let/...
 -- It makes sure the "continuation" `?_` is the main goal after refining
-macro "refine_lift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotate_right))
+macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right))
 
 macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
 /- We use a priority > default, to avoid ambiguity with previous `have` notation -/
@@ -372,7 +372,7 @@ macro_rules
   | `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
 
 -- Similar to `refineLift`, but using `refine'`
-macro "refine_lift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotate_right))
+macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right))
 macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
 macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 0c3bef1cfb..c829509a01 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -275,7 +275,7 @@ def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax
   let yName := y.getId
   let doElem ← `(doElem| let y ← $e:term)
   -- Add elaboration hint for producing sane error message
-  let y ← `(ensureExpectedType% "type mismatch, result value" $y)
+  let y ← `(ensure_expected_type% "type mismatch, result value" $y)
   let k ← mkCont y
   pure $ Code.decl #[yName] doElem k
 
@@ -977,7 +977,7 @@ def reassignToTerm (reassign : Syntax) (k : Syntax) : MacroM Syntax := withRef r
       -- letIdDecl := leading_parser ident >> many (ppSpace >> bracketedBinder) >> optType >>  " := " >> termParser
       let x   := arg[0]
       let val := arg[4]
-      let newVal ← `(ensureTypeOf% $x $(quote "invalid reassignment, value") $val)
+      let newVal ← `(ensure_type_of% $x $(quote "invalid reassignment, value") $val)
       let arg := arg.setArg 4 newVal
       let letDecl := mkNode `Lean.Parser.Term.letDecl #[arg]
       `(let $letDecl:letDecl; $k)
@@ -997,7 +997,7 @@ def mkIte (optIdent : Syntax) (cond : Syntax) (thenBranch : Syntax) (elseBranch
     ``(if $h:ident : $cond then $thenBranch else $elseBranch)
 
 def mkJoinPoint (j : Name) (ps : Array (Name × Bool)) (body : Syntax) (k : Syntax) : M Syntax := withRef body <| withFreshMacroScope do
-  let pTypes ← ps.mapM fun ⟨id, useTypeOf⟩ => do if useTypeOf then `(typeOf% $(← mkIdentFromRef id)) else `(_)
+  let pTypes ← ps.mapM fun ⟨id, useTypeOf⟩ => do if useTypeOf then `(type_of% $(← mkIdentFromRef id)) else `(_)
   let ps     ← ps.mapM fun ⟨id, useTypeOf⟩ => mkIdentFromRef id
   /-
   We use `let_delayed` instead of `let` for joinpoints to make sure `$k` is elaborated before `$body`.
@@ -1417,20 +1417,20 @@ mutual
       let uvarsTuple ← liftMacroM do mkTuple (← uvars.mapM mkIdentFromRef)
       if hasReturn forInBodyCodeBlock.code then
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
+        let forInTerm ← `(for_in% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
         let auxDo ← `(do let r ← $forInTerm:term;
                          $uvarsTuple:term := r.2;
                          match r.1 with
-                         | none => Pure.pure (ensureExpectedType% "type mismatch, 'for'" PUnit.unit)
-                         | some a => return ensureExpectedType% "type mismatch, 'for'" a)
+                         | none => Pure.pure (ensure_expected_type% "type mismatch, 'for'" PUnit.unit)
+                         | some a => return ensure_expected_type% "type mismatch, 'for'" a)
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
       else
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn% $(xs) $uvarsTuple fun $x r => $forInBody)
+        let forInTerm ← `(for_in% $(xs) $uvarsTuple fun $x r => $forInBody)
         if doElems.isEmpty then
           let auxDo ← `(do let r ← $forInTerm:term;
                            $uvarsTuple:term := r;
-                           Pure.pure (ensureExpectedType% "type mismatch, 'for'" PUnit.unit))
+                           Pure.pure (ensure_expected_type% "type mismatch, 'for'" PUnit.unit))
           doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
         else
           let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 4504462a3f..c26ec6c940 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -45,9 +45,9 @@ open Meta
 
 @[builtinTermElab forInMacro] def elabForIn : TermElab :=  fun stx expectedType? => do
   match stx with
-  | `(forIn% $col $init $body) =>
+  | `(for_in% $col $init $body) =>
       match (← isLocalIdent? col) with
-      | none   => elabTerm (← `(let col := $col; forIn% col $init $body)) expectedType?
+      | none   => elabTerm (← `(let col := $col; for_in% col $init $body)) expectedType?
       | some colFVar =>
         tryPostponeIfNoneOrMVar expectedType?
         let m ← getMonad expectedType?
@@ -69,13 +69,13 @@ open Meta
 where
   getMonad (expectedType? : Option Expr) : TermElabM Expr := do
     match expectedType? with
-    | none => throwError "invalid 'forIn%' notation, expected type is not available"
+    | none => throwError "invalid 'for_in%' notation, expected type is not available"
     | some expectedType =>
       match (← isTypeApp? expectedType) with
       | some (m, _) => return m
-      | none => throwError "invalid 'forIn%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
+      | none => throwError "invalid 'for_in%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
   throwFailure (forInInstance : Expr) : TermElabM Expr :=
-    throwError "failed to synthesize instance for 'forIn%' notation{indentExpr forInInstance}"
+    throwError "failed to synthesize instance for 'for_in%' notation{indentExpr forInInstance}"
 
 namespace BinOp
 /-
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 057301141a..d45a8377f9 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1121,7 +1121,7 @@ private def isTacticBlock (stx : Syntax) : Bool :=
 
 private def isNoImplicitLambda (stx : Syntax) : Bool :=
   match stx with
-  | `(noImplicitLambda% $x:term) => true
+  | `(no_implicit_lambda% $x:term) => true
   | _ => false
 
 private def isTypeAscription (stx : Syntax) : Bool :=
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 3b08e989a6..beb49361b6 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -207,12 +207,12 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 @[builtinTermParser] def binop  := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
 @[builtinTermParser] def binop_lazy  := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
 
-@[builtinTermParser] def forInMacro := leading_parser ("forIn% " <|> "for_in% ") >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
+@[builtinTermParser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
 
-@[builtinTermParser] def typeOf             := leading_parser ("typeOf% " <|> "type_of% ") >> termParser maxPrec
-@[builtinTermParser] def ensureTypeOf       := leading_parser ("ensureTypeOf% " <|> "ensure_type_of% ") >> termParser maxPrec >> strLit >> termParser
-@[builtinTermParser] def ensureExpectedType := leading_parser ("ensureExpectedType% " <|> "ensure_expected_type% ") >> strLit >> termParser maxPrec
-@[builtinTermParser] def noImplicitLambda   := leading_parser ("noImplicitLambda% " <|> "no_implicit_lambda% ") >> termParser maxPrec
+@[builtinTermParser] def typeOf             := leading_parser "type_of% " >> termParser maxPrec
+@[builtinTermParser] def ensureTypeOf       := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
+@[builtinTermParser] def ensureExpectedType := leading_parser "ensure_expected_type% " >> strLit >> termParser maxPrec
+@[builtinTermParser] def noImplicitLambda   := leading_parser "no_implicit_lambda% " >> termParser maxPrec
 
 def namedArgument  := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := leading_parser ".."
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 9ebe9ed329..7b4822bf92 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -228,7 +228,7 @@ def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoic
 
 partial instance : ForIn m TopDown Syntax where
   forIn := fun ⟨firstChoiceOnly, stx⟩ init f => do
-    let rec @[specialize] loop stx b [Inhabited (typeOf% b)] := do
+    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
       match (← f stx b) with
       | ForInStep.yield b' =>
         let mut b := b'
diff --git a/tests/lean/run/impLambdaTac.lean b/tests/lean/run/impLambdaTac.lean
index aaced11641..40c0a8f1c1 100644
--- a/tests/lean/run/impLambdaTac.lean
+++ b/tests/lean/run/impLambdaTac.lean
@@ -8,9 +8,9 @@ example (P : Prop) : ∀ {p : P}, P := by
   exact @id _
 
 example (P : Prop) : ∀ {p : P}, P := by
-  exact noImplicitLambda% id
+  exact no_implicit_lambda% id
 
-macro "exact'" x:term : tactic => `(exact noImplicitLambda% $x)
+macro "exact'" x:term : tactic => `(exact no_implicit_lambda% $x)
 
 example (P : Prop) : ∀ {p : P}, P := by
   exact' id
@@ -23,7 +23,7 @@ example (P : Prop) : ∀ p : P, P := by
   apply id
 
 example (P : Prop) : ∀ {p : P}, P := by
-  refine noImplicitLambda% (have : _ := 1; ?_)
+  refine no_implicit_lambda% (have : _ := 1; ?_)
   apply id
 
 example (P : Prop) : ∀ {p : P}, P := by
diff --git a/tests/lean/typeOf.lean b/tests/lean/typeOf.lean
index 357b0caff9..20f9f672a6 100644
--- a/tests/lean/typeOf.lean
+++ b/tests/lean/typeOf.lean
@@ -1,29 +1,29 @@
 --
 
-def f1 (x : Nat) (b : Bool) : typeOf% x :=
-let r : typeOf% (x+1) := x+1;
+def f1 (x : Nat) (b : Bool) : type_of% x :=
+let r : type_of% (x+1) := x+1;
 r + 1
 
 theorem ex1 : f1 1 true = 3 :=
 rfl
 
-def f2 (x : Nat) (b : Bool) : typeOf% x :=
-let r : typeOf% b := x+1; -- error
+def f2 (x : Nat) (b : Bool) : type_of% x :=
+let r : type_of% b := x+1; -- error
 r + 1
 
-def f3 (x : Nat) (b : Bool) : typeOf% b :=
-let r (x!1 : typeOf% x) : typeOf% b := x > 1;
+def f3 (x : Nat) (b : Bool) : type_of% b :=
+let r (x!1 : type_of% x) : type_of% b := x > 1;
 r x
 
 def f4 (x : Nat) : Nat :=
 let y : Nat := x
-let y := ensureTypeOf% y "invalid reassignment, term" y == 1 -- error
+let y := ensure_type_of% y "invalid reassignment, term" y == 1 -- error
 y + 1
 
 def f5 (x : Nat) : Nat :=
 let y : Nat := x
-let y := ensureTypeOf% y "invalid reassignment, term" (y+1)
+let y := ensure_type_of% y "invalid reassignment, term" (y+1)
 y + 1
 
 def f6 (x : Nat) : Nat :=
-ensureExpectedType% "natural number expected, value" true
+ensure_expected_type% "natural number expected, value" true
diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out
index eff0a58127..12b0b73d8f 100644
--- a/tests/lean/typeOf.lean.expected.out
+++ b/tests/lean/typeOf.lean.expected.out
@@ -1,12 +1,12 @@
-typeOf.lean:11:21-11:24: error: failed to synthesize instance
+typeOf.lean:11:22-11:25: error: failed to synthesize instance
   HAdd Nat Nat Bool
 typeOf.lean:12:0-12:5: error: failed to synthesize instance
   HAdd Bool Nat Nat
-typeOf.lean:20:54-20:60: error: invalid reassignment, term has type
+typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type
 but is expected to have type
   Nat : Type
-typeOf.lean:29:53-29:57: error: natural number expected, value has type
+typeOf.lean:29:55-29:59: error: natural number expected, value has type
   Bool : Type
 but is expected to have type
   Nat : Type