diff --git a/library/init/IO.lean b/library/init/IO.lean
index e28db51ef8..83e2322b81 100644
--- a/library/init/IO.lean
+++ b/library/init/IO.lean
@@ -186,7 +186,7 @@ end Proc
 
 /- References -/
 constant RefPointed : PointedType := default _
-def Ref (α : Type) : Type := RefPointed.Type
+def Ref (α : Type) : Type := RefPointed.type
 instance (α : Type) : Inhabited (Ref α) :=
 ⟨RefPointed.val⟩
 
diff --git a/library/init/Lean/declaration.lean b/library/init/Lean/declaration.lean
index 5598fe2889..838031943b 100644
--- a/library/init/Lean/declaration.lean
+++ b/library/init/Lean/declaration.lean
@@ -38,7 +38,7 @@ inductive ReducibilityHints
 
 /-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `inductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`. -/
 structure ConstantVal :=
-(id : Name) (lparams : List Name) (Type : Expr)
+(id : Name) (lparams : List Name) (type : Expr)
 
 structure AxiomVal extends ConstantVal :=
 (isUnsafe : Bool)
@@ -54,10 +54,10 @@ structure OpaqueVal extends ConstantVal :=
 (value : Expr)
 
 structure Constructor :=
-(id : Name) (Type : Expr)
+(id : Name) (type : Expr)
 
 structure inductiveType :=
-(id : Name) (Type : Expr) (cnstrs : List Constructor)
+(id : Name) (type : Expr) (cnstrs : List Constructor)
 
 /-- Declaration object that can be sent to the kernel. -/
 inductive Declaration
@@ -112,7 +112,7 @@ structure RecursorVal extends ConstantVal :=
 (isUnsafe : Bool)
 
 inductive QuotKind
-| Type  -- `Quot`
+| type  -- `Quot`
 | cnstr -- `Quot.mk`
 | lift  -- `Quot.lift`
 | ind   -- `Quot.ind`
diff --git a/library/init/Lean/util.lean b/library/init/Lean/util.lean
index f772db3ad9..6d6be4bf2e 100644
--- a/library/init/Lean/util.lean
+++ b/library/init/Lean/util.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich
 -/
 prelude
-import init.Lean.Position init.Io
+import init.Lean.Position init.IO
 
 namespace Lean
 
 /-- Print and accumulate run time of `act` when Option `profiler` is set to `True`. -/
 @[extern 5 "lean_lean_profileit"]
-constant profileit {α : Type} (category : @& String) (pos : @& Position) (act : Io α) : Io α := act
-def profileitPure {α : Type} (category : String) (pos : Position) (fn : unit → α) : Io α :=
-profileit category pos $ Io.lazyPure fn
+constant profileit {α : Type} (category : @& String) (pos : @& Position) (act : IO α) : IO α := act
+def profileitPure {α : Type} (category : String) (pos : Position) (fn : unit → α) : IO α :=
+profileit category pos $ IO.lazyPure fn
 
 end Lean
diff --git a/library/init/control/State.lean b/library/init/control/State.lean
index f0450470ca..d7b3ab0a02 100644
--- a/library/init/control/State.lean
+++ b/library/init/control/State.lean
@@ -151,8 +151,8 @@ export MonadStateAdapter (adaptState)
 section
 variables {σ σ' : Type u} {m m' : Type u → Type v}
 
-def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toΣ : σ' → σ) (fromΣ : σ → σ') : m α → m' α :=
-adaptState (λ st, (toΣ st, Punit.star)) (λ st _, fromΣ st)
+def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α :=
+adaptState (λ st, (toSigma st, Punit.star)) (λ st _, fromSigma st)
 export MonadStateAdapter (adaptState')
 
 instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index 6b2aafe6c1..61bf84afcd 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -8,7 +8,7 @@ import init.data.Nat.div init.data.Nat.bitwise
 open Nat
 structure Fin (n : Nat) := (val : Nat) (isLt : val < n)
 
-attribute [ppUsingAnonymousConstructor] Fin
+attribute [ppAnonymousCtor] Fin
 
 namespace Fin
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 557a94ae85..b3392c3f57 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -550,7 +550,7 @@ optional<expr> elaborator::mk_coercion_core(expr const & e, expr const & e_type,
     if (e_type == mk_Prop() && m_ctx.is_def_eq(type, mk_bool())) {
         return mk_Prop_to_bool_coercion(e, ref);
     } else if (is_thunk(type) && m_ctx.is_def_eq(e_type, app_arg(type))) {
-        return some_expr(::lean::mk_app(mk_constant(name{"thunk", "mk"}, const_levels(app_fn(type))),
+        return some_expr(::lean::mk_app(mk_constant(name{"Thunk", "mk"}, const_levels(app_fn(type))),
                                         app_arg(type),
                                         ::lean::mk_lambda("_", mk_constant(get_unit_name()), e)));
     } else if (!has_expr_metavar(e_type) && !has_expr_metavar(type)) {
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 292cd098a1..aeff83715b 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -841,8 +841,8 @@ void initialize_expr() {
     g_Prop         = new expr(mk_sort(mk_level_zero()));
     /* TODO(Leo): add support for builtin constants in the kernel.
        Something similar to what we have in the library directory. */
-    g_nat_type     = new expr(mk_constant("nat"));
-    g_string_type  = new expr(mk_constant("string"));
+    g_nat_type     = new expr(mk_constant("Nat"));
+    g_string_type  = new expr(mk_constant("String"));
 }
 
 void finalize_expr() {