diff --git a/library/init/control/except.lean b/library/init/control/except.lean
index c4f9a4c202..dec0f4348f 100644
--- a/library/init/control/except.lean
+++ b/library/init/control/except.lean
@@ -34,39 +34,39 @@ end
 
 namespace except
 section
-  parameter {ε : Type u}
+parameter {ε : Type u}
 
-  protected def return {α : Type v} (a : α) : except ε α :=
-  except.ok a
+@[inline] protected def return {α : Type v} (a : α) : except ε α :=
+except.ok a
 
-  protected def map {α β : Type v} (f : α → β) : except ε α → except ε β
-  | (except.error err) := except.error err
-  | (except.ok v) := except.ok $ f v
+@[inline] protected def map {α β : Type v} (f : α → β) : except ε α → except ε β
+| (except.error err) := except.error err
+| (except.ok v) := except.ok $ f v
 
-  protected def map_error {ε' : Type u} {α : Type v} (f : ε → ε') : except ε α → except ε' α
-  | (except.error err) := except.error $ f err
-  | (except.ok v) := except.ok v
+@[inline] protected def map_error {ε' : Type u} {α : Type v} (f : ε → ε') : except ε α → except ε' α
+| (except.error err) := except.error $ f err
+| (except.ok v) := except.ok v
 
-  protected def bind {α β : Type v} (ma : except ε α) (f : α → except ε β) : except ε β :=
-  match ma with
-  | (except.error err) := except.error err
-  | (except.ok v) := f v
+@[inline] protected def bind {α β : Type v} (ma : except ε α) (f : α → except ε β) : except ε β :=
+match ma with
+| (except.error err) := except.error err
+| (except.ok v) := f v
 
-  protected def to_bool {α : Type v} : except ε α → bool
-  | (except.ok _)    := tt
-  | (except.error _) := ff
+@[inline] protected def to_bool {α : Type v} : except ε α → bool
+| (except.ok _)    := tt
+| (except.error _) := ff
 
-  protected def to_option {α : Type v} : except ε α → option α
-  | (except.ok a)    := some a
-  | (except.error _) := none
+@[inline] protected def to_option {α : Type v} : except ε α → option α
+| (except.ok a)    := some a
+| (except.error _) := none
 
-  protected def catch {α : Type u} (ma : except ε α) (handle : ε → except ε α) : except ε α :=
-  match ma with
-  | except.ok a    := except.ok a
-  | except.error e := handle e
+@[inline] protected def catch {α : Type u} (ma : except ε α) (handle : ε → except ε α) : except ε α :=
+match ma with
+| except.ok a    := except.ok a
+| except.error e := handle e
 
-  instance : monad (except ε) :=
-  { pure := @return, bind := @bind }
+instance : monad (except ε) :=
+{ pure := @return, bind := @bind }
 end
 end except
 
@@ -78,43 +78,43 @@ attribute [pp_using_anonymous_constructor] except_t
 
 namespace except_t
 section
-  parameters {ε : Type u} {m : Type u → Type v} [monad m]
+parameters {ε : Type u} {m : Type u → Type v} [monad m]
 
-  @[inline] protected def return {α : Type u} (a : α) : except_t ε m α :=
-  ⟨pure $ except.ok a⟩
+@[inline] protected def return {α : Type u} (a : α) : except_t ε m α :=
+⟨pure $ except.ok a⟩
 
-  @[inline] protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
-  | (except.ok a)    := (f a).run
-  | (except.error e) := pure (except.error e)
+@[inline] protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
+| (except.ok a)    := (f a).run
+| (except.error e) := pure (except.error e)
 
-  @[inline] protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
-  ⟨ma.run >>= bind_cont f⟩
+@[inline] protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
+⟨ma.run >>= bind_cont f⟩
 
-  @[inline] protected def lift {α : Type u} (t : m α) : except_t ε m α :=
-  ⟨except.ok <$> t⟩
+@[inline] protected def lift {α : Type u} (t : m α) : except_t ε m α :=
+⟨except.ok <$> t⟩
 
-  instance except_t_of_except : has_monad_lift (except ε) (except_t ε m) :=
-  ⟨λ α e, ⟨pure e⟩⟩
+instance except_t_of_except : has_monad_lift (except ε) (except_t ε m) :=
+⟨λ α e, ⟨pure e⟩⟩
 
-  instance : has_monad_lift m (except_t ε m) :=
-  ⟨@except_t.lift⟩
+instance : has_monad_lift m (except_t ε m) :=
+⟨@except_t.lift⟩
 
-  protected def catch {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) : except_t ε m α :=
-  ⟨ma.run >>= λ res, match res with
-   | except.ok a    := pure (except.ok a)
-   | except.error e := (handle e).run⟩
+@[inline] protected def catch {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) : except_t ε m α :=
+⟨ma.run >>= λ res, match res with
+| except.ok a    := pure (except.ok a)
+| except.error e := (handle e).run⟩
 
-  @[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
-  λ x, ⟨f x.run⟩
+@[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
+λ x, ⟨f x.run⟩
 
-  instance (m') [monad m'] : monad_functor m m' (except_t ε m) (except_t ε m') :=
-  ⟨@monad_map m' _⟩
+instance (m') [monad m'] : monad_functor m m' (except_t ε m) (except_t ε m') :=
+⟨@monad_map m' _⟩
 
-  instance : monad (except_t ε m) :=
-  { pure := @return, bind := @bind }
+instance : monad (except_t ε m) :=
+{ pure := @return, bind := @bind }
 
-  @[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : except_t ε m α → except_t ε' m α :=
-  λ x, ⟨except.map_error f <$> x.run⟩
+@[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : except_t ε m α → except_t ε' m α :=
+λ x, ⟨except.map_error f <$> x.run⟩
 end
 end except_t
 
@@ -127,15 +127,15 @@ class monad_except (ε : out_param (Type u)) (m : Type v → Type w) :=
 namespace monad_except
 variables {ε : Type u} {m : Type v → Type w}
 
-protected def orelse [monad_except ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
+@[inline] protected def orelse [monad_except ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
 catch t₁ $ λ _, t₂
 
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/
-def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α :=
+@[inline] def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α :=
 catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if use_first_ex then e₁ else e₂)
 
-def lift_except {ε' : Type u} [monad_except ε m] [has_lift_t ε' ε] [monad m] {α : Type v} : except ε' α → m α
+@[inline] def lift_except {ε' : Type u} [monad_except ε m] [has_lift_t ε' ε] [monad m] {α : Type v} : except ε' α → m α
 | (except.error e) := throw ↑e
 | (except.ok a)    := pure a
 end monad_except