diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean
index 71a74620d1..57d8e36fe0 100644
--- a/library/standard/data/nat/basic.lean
+++ b/library/standard/data/nat/basic.lean
@@ -62,7 +62,7 @@ calc_subst subst
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
 assume H : succ n = 0,
 have H2 : true = false, from
-  let f [inline] := (nat_rec false (fun a b, true)) in
+  let f := (nat_rec false (fun a b, true)) in
     calc
       true = f (succ n) : rfl
        ... = f 0        : {H}
@@ -115,19 +115,19 @@ have general : ∀n, decidable (n = m), from
   rec_on m
     (take n,
       rec_on n
-	(inl (refl 0))
-	(λ m iH, inr (succ_ne_zero m)))
+        (inl (refl 0))
+        (λ m iH, inr (succ_ne_zero m)))
     (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')),
       take n, rec_on n
-	(inr (ne_symm (succ_ne_zero m')))
-	(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
-	  have d1 : decidable (n' = m'), from iH1 n',
-	  decidable.rec_on d1
-	    (assume Heq : n' = m', inl (congr_arg succ Heq))
-	    (assume Hne : n' ≠ m',
-	      have H1 : succ n' ≠ succ m', from
-		assume Heq, absurd (succ_inj Heq) Hne,
-	      inr H1))),
+        (inr (ne_symm (succ_ne_zero m')))
+        (λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
+          have d1 : decidable (n' = m'), from iH1 n',
+          decidable.rec_on d1
+            (assume Heq : n' = m', inl (congr_arg succ Heq))
+            (assume Hne : n' ≠ m',
+              have H1 : succ n' ≠ succ m', from
+                assume Heq, absurd (succ_inj Heq) Hne,
+              inr H1))),
 general n
 
 theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
@@ -138,7 +138,7 @@ have stronger : P a ∧ P (succ a), from
     (take k IH,
       have IH1 : P k, from and_elim_left IH,
       have IH2 : P (succ k), from and_elim_right IH,
-	and_intro IH2 (H3 k IH1 IH2)),
+        and_intro IH2 (H3 k IH1 IH2)),
   and_elim_left stronger
 
 theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
@@ -150,10 +150,10 @@ have general : ∀m, P n m, from induction_on n
     take m : ℕ,
     discriminate
       (assume Hm : m = 0,
-	Hm⁻¹ ▸ (H2 k))
+        Hm⁻¹ ▸ (H2 k))
       (take l : ℕ,
-	assume Hm : m = succ l,
-	  Hm⁻¹ ▸ (H3 k l (IH l)))),
+        assume Hm : m = succ l,
+          Hm⁻¹ ▸ (H3 k l (IH l)))),
 general m
 
 
@@ -237,14 +237,14 @@ induction_on n
   (take H : 0 + m = 0 + k,
     calc
       m = 0 + m : symm (add_zero_left m)
-	... = 0 + k : H
-	... = k : add_zero_left k)
+        ... = 0 + k : H
+        ... = k : add_zero_left k)
   (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
     have H2 : succ (n + m) = succ (n + k),
     from calc
       succ (n + m) = succ n + m : symm (add_succ_left n m)
-	... = succ n + k : H
-	... = succ (n + k) : add_succ_left n k,
+        ... = succ n + k : H
+        ... = succ (n + k) : add_succ_left n k,
     have H3 : n + m = n + k, from succ_inj H2,
     IH H3)
 
@@ -263,9 +263,9 @@ induction_on n
     assume (H : succ k + m = 0),
     absurd_elim (succ k = 0)
       (show succ (k + m) = 0, from
-	calc
-	  succ (k + m) = succ k + m : symm (add_succ_left k m)
-	    ... = 0 : H)
+        calc
+          succ (k + m) = succ k + m : symm (add_succ_left k m)
+            ... = 0 : H)
       (succ_ne_zero (k + m)))
 
 theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 :=
@@ -313,8 +313,8 @@ induction_on n
   (take m IH,
     calc
       0 * succ m = 0 * m + 0 : mul_succ_right _ _
-	... = 0 * m : add_zero_right _
-	... = 0 : IH)
+        ... = 0 * m : add_zero_right _
+        ... = 0 : IH)
 
 theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m :=
 induction_on m
@@ -325,11 +325,11 @@ induction_on m
   (take k IH,
     calc
       succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
-	  ... = (n * k) + k + succ n : { IH }
-	  ... = (n * k) + (k + succ n) : add_assoc _ _ _
-	  ... = (n * k) + (n + succ k) : {add_comm_succ _ _}
-	  ... = (n * k) + n + succ k : symm (add_assoc _ _ _)
-	  ... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
+          ... = (n * k) + k + succ n : { IH }
+          ... = (n * k) + (k + succ n) : add_assoc _ _ _
+          ... = (n * k) + (n + succ k) : {add_comm_succ _ _}
+          ... = (n * k) + n + succ k : symm (add_assoc _ _ _)
+          ... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
 
 theorem mul_comm (n m:ℕ) : n * m = m * n :=
 induction_on m
@@ -337,8 +337,8 @@ induction_on m
   (take k IH,
     calc
       n * succ k = n * k + n : mul_succ_right _ _
-	... = k * n + n : {IH}
-	... = (succ k) * n : symm (mul_succ_left _ _))
+        ... = k * n + n : {IH}
+        ... = (succ k) * n : symm (mul_succ_left _ _))
 
 theorem mul_distr_right (n m k : ℕ) : (n + m) * k = n * k + m * k :=
 induction_on k
@@ -349,12 +349,12 @@ induction_on k
       ... = n * 0 + m * 0 : {symm (mul_zero_right _)})
   (take l IH, calc
       (n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
-	... = n * l + m * l + (n + m) : {IH}
-	... = n * l + m * l + n + m : symm (add_assoc _ _ _)
-	... = n * l + n + m * l + m : {add_right_comm _ _ _}
-	... = n * l + n + (m * l + m) : add_assoc _ _ _
-	... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
-	... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
+        ... = n * l + m * l + (n + m) : {IH}
+        ... = n * l + m * l + n + m : symm (add_assoc _ _ _)
+        ... = n * l + n + m * l + m : {add_right_comm _ _ _}
+        ... = n * l + n + (m * l + m) : add_assoc _ _ _
+        ... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
+        ... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
 
 theorem mul_distr_left (n m k : ℕ) : n * (m + k) = n * m + n * k :=
 calc
@@ -372,9 +372,9 @@ induction_on k
   (take l IH,
     calc
       (n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _
-	... = n * (m * l) + n * m : {IH}
-	... = n * (m * l + m) : symm (mul_distr_left _ _ _)
-	... = n * (m * succ l) : {symm (mul_succ_right _ _)})
+        ... = n * (m * l) + n * m : {IH}
+        ... = n * (m * l + m) : symm (mul_distr_left _ _ _)
+        ... = n * (m * succ l) : {symm (mul_succ_right _ _)})
 
 theorem mul_left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) :=
 left_comm mul_comm mul_assoc n m k
@@ -401,14 +401,14 @@ discriminate
     discriminate
       (take (Hm : m = 0), or_intro_right _ Hm)
       (take (l : ℕ),
-	assume (Hl : m = succ l),
-	have Heq : succ (k * succ l + l) = n * m, from
-	  symm (calc
-	    n * m = n * succ l : {Hl}
-	      ... = succ k * succ l : {Hk}
-	      ... = k * succ l + succ l : mul_succ_left _ _
-	      ... = succ (k * succ l + l) : add_succ_right _ _),
-	absurd_elim _  (trans Heq H) (succ_ne_zero _)))
+        assume (Hl : m = succ l),
+        have Heq : succ (k * succ l + l) = n * m, from
+          symm (calc
+            n * m = n * succ l : {Hl}
+              ... = succ k * succ l : {Hk}
+              ... = k * succ l + succ l : mul_succ_left _ _
+              ... = succ (k * succ l + l) : add_succ_right _ _),
+        absurd_elim _  (trans Heq H) (succ_ne_zero _)))
 
 ---other inversion theorems appear below
 
diff --git a/library/standard/data/nat/div.lean b/library/standard/data/nat/div.lean
index 6dff9128ed..56df2e6495 100644
--- a/library/standard/data/nat/div.lean
+++ b/library/standard/data/nat/div.lean
@@ -87,8 +87,8 @@ theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom
   let f := rec_measure default measure rec_val in
   f' m = restrict default measure f m :=
 -- TODO: note the use of (need for) inline here
-let f' [inline] := rec_measure_aux default measure rec_val in
-let f [inline] := rec_measure default measure rec_val in
+let f' := rec_measure_aux default measure rec_val in
+let f  := rec_measure default measure rec_val in
 case_strong_induction_on m
   (have H1 : f' 0 = (λx, default), from rfl,
     have H2 : restrict default measure f 0 = (λx, default), from
@@ -111,7 +111,7 @@ case_strong_induction_on m
                     ... = rec_val x (restrict default measure f m) : {IH m (le_refl m)}
                     ... = rec_val x f : symm (rec_decreasing _ _ _ (lt_succ_imp_le H1)),
               have H3 : restrict default measure f (succ m) x = rec_val x f, from
-                let m' [inline] := measure x in
+                let m' := measure x in
                 calc
                   restrict default measure f (succ m) x = f x : if_pos H1 _ _
                     ... = f' (succ m') x : refl _
@@ -138,9 +138,9 @@ theorem rec_measure_spec {dom codom : Type} {default : codom} {measure : dom →
     (x : dom):
   let f := rec_measure default measure rec_val in
   f x = rec_val x f :=
-let f' [inline] := rec_measure_aux default measure rec_val in
-let f [inline] := rec_measure default measure rec_val in
-let m [inline] := measure x in
+let f' := rec_measure_aux default measure rec_val in
+let f  := rec_measure default measure rec_val in
+let m  := measure x in
 calc
   f x = f' (succ m) x : refl _
     ... = if measure x < succ m then rec_val x (f' m) else default : rfl
@@ -162,8 +162,8 @@ definition div_aux (y : ℕ) : ℕ → ℕ := rec_measure 0 (fun x, x) (div_aux_
 
 theorem div_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H : m ≥ x) :
   div_aux_rec y x g = div_aux_rec y x (restrict 0 (fun x, x) g m) :=
-let lhs [inline] := div_aux_rec y x g in
-let rhs [inline] := div_aux_rec y x (restrict 0 (fun x, x) g m) in
+let lhs := div_aux_rec y x g in
+let rhs := div_aux_rec y x (restrict 0 (fun x, x) g m) in
 show lhs = rhs, from
   by_cases (y = 0 ∨ x < y)
     (assume H1 : y = 0 ∨ x < y,
@@ -238,8 +238,8 @@ definition mod_aux (y : ℕ) : ℕ → ℕ := rec_measure 0 (fun x, x) (mod_aux_
 
 theorem mod_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H : m ≥ x) :
   mod_aux_rec y x g = mod_aux_rec y x (restrict 0 (fun x, x) g m) :=
-let lhs [inline] := mod_aux_rec y x g in
-let rhs [inline] := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
+let lhs := mod_aux_rec y x g in
+let rhs := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
 show lhs = rhs, from
   by_cases (y = 0 ∨ x < y)
     (assume H1 : y = 0 ∨ x < y,
@@ -596,17 +596,17 @@ definition gcd_aux_measure (p : ℕ × ℕ) : ℕ :=
 pr2 p
 
 definition gcd_aux_rec (p : ℕ × ℕ) (gcd_aux' : ℕ × ℕ → ℕ) : ℕ :=
-let x [inline] := pr1 p, y [inline] := pr2 p in
+let x := pr1 p, y := pr2 p in
 if y = 0 then x else gcd_aux' (pair y (x mod y))
 
 definition gcd_aux : ℕ × ℕ → ℕ := rec_measure 0 gcd_aux_measure gcd_aux_rec
 
 theorem gcd_aux_decreasing (g : ℕ × ℕ → ℕ) (m : ℕ) (p : ℕ × ℕ) (H : m ≥ gcd_aux_measure p) :
   gcd_aux_rec p g = gcd_aux_rec p (restrict 0 gcd_aux_measure g m) :=
-let x [inline] := pr1 p, y [inline] := pr2 p in
-let p' [inline] := pair y (x mod y) in
-let lhs [inline] := gcd_aux_rec p g in
-let rhs [inline] := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
+let x := pr1 p, y := pr2 p in
+let p' := pair y (x mod y) in
+let lhs := gcd_aux_rec p g in
+let rhs := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
 show lhs = rhs, from
   by_cases (y = 0)
     (assume H1 : y = 0,
@@ -624,14 +624,14 @@ show lhs = rhs, from
           ... = lhs : symm (if_neg H1 _ _)))
 
 theorem gcd_aux_spec (p : ℕ × ℕ) : gcd_aux p =
-let x [inline] := pr1 p, y [inline] := pr2 p in
+let x := pr1 p, y := pr2 p in
 if y = 0 then x else gcd_aux (pair y (x mod y)) :=
 rec_measure_spec gcd_aux_rec gcd_aux_decreasing p
 
 definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)
 
 theorem gcd_def (x y : ℕ) : gcd x y = if y = 0 then x else gcd y (x mod y) :=
-let x' [inline] := pr1 (pair x y), y' [inline] := pr2 (pair x y) in
+let x' := pr1 (pair x y), y' := pr2 (pair x y) in
 calc
   gcd x y = if y' = 0 then x' else gcd_aux (pair y' (x' mod y'))
       : gcd_aux_spec (pair x y)
diff --git a/library/standard/data/quotient/basic.lean b/library/standard/data/quotient/basic.lean
index 651484e930..4d1bf31f57 100644
--- a/library/standard/data/quotient/basic.lean
+++ b/library/standard/data/quotient/basic.lean
@@ -27,7 +27,7 @@ abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (re
 
 theorem intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (H1 : ∀b, abs (rep b) = b) (H2 : ∀b, R (rep b) (rep b))
-  (H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep := 
+  (H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep :=
 and_intro H1 (and_intro H2 H3)
 
 theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
@@ -41,16 +41,16 @@ intro
   (take b, H1 (rep b))
   (take r s,
     have H4 : R r s ↔ R s s ∧ abs r = abs s,
-      from 
+      from
         subst (symm (and_absorb_left _ (H1 s))) (H3 r s),
     subst (symm (and_absorb_left _ (H1 r))) H4)
 
 theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
-  (Q : is_quotient R abs rep) (b : B) :  abs (rep b) = b := 
+  (Q : is_quotient R abs rep) (b : B) :  abs (rep b) = b :=
 and_elim_left Q b
 
 theorem refl_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
-  (Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) := 
+  (Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) :=
 and_elim_left (and_elim_right Q) b
 
 theorem R_iff {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
@@ -124,7 +124,7 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
 have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha,
 calc
-  rec Q f (abs a) =  eq_rec_on _ (f (rep (abs a))) : rfl 
+  rec Q f (abs a) =  eq_rec_on _ (f (rep (abs a))) : rfl
     ... = eq_rec_on _ (eq_rec_on _ (f a)) : {symm (H _ _ H2)}
     ... = eq_rec_on _ (f a) : eq_rec_on_compose _ _ _
     ... = f a : eq_rec_on_id _ _
@@ -213,7 +213,7 @@ image_inhabited f (inhabited_mk a)
 definition fun_image {A B : Type} (f : A → B) (a : A) : image f :=
 tag (f a) (exists_intro a rfl)
 
-theorem fun_image_def {A B : Type} (f : A → B) (a : A) : 
+theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
   fun_image f a = tag (f a) (exists_intro a rfl) := rfl
 
 theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a :=
@@ -223,7 +223,7 @@ theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_
 has_property u
 
 theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_image f a = u :=
-subtype_destruct u 
+subtype_destruct u
   (take (b : B) (H : ∃a, f a = b),
     obtain a (H': f a = b), from H,
     (exists_intro a (tag_eq H')))
@@ -273,7 +273,7 @@ symm (H2 a (f a) (H1 a))
 theorem representative_map_refl_rep {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) :
   R (f a) (f a) :=
-subst (representative_map_idempotent H1 H2 a) (H1 (f a)) 
+subst (representative_map_idempotent H1 H2 a) (H1 (f a))
 
 theorem representative_map_image_fix {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') (b : image f) :
@@ -283,7 +283,7 @@ idempotent_image_fix (representative_map_idempotent H1 H2) b
 theorem representative_map_to_quotient {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') :
   is_quotient _ (fun_image f) elt_of :=
-let abs [inline] := fun_image f in
+let abs := fun_image f in
 intro
   (take u : image f,
     obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
@@ -298,12 +298,12 @@ intro
     show R (elt_of u) (elt_of u), from
       obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
         subst Ha (@representative_map_refl_rep A R f H1 H2 a))
-  (take a a', 
+  (take a a',
     subst (fun_image_eq f a a') (H2 a a'))
 
 theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop}
-    (equiv : is_equivalence R) {f : A → A} 
-    (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) : 
+    (equiv : is_equivalence R) {f : A → A}
+    (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) :
   R a b :=
 have symmR : symmetric R, from rel_symm R,
 have transR : transitive R, from rel_trans R,
diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean
index 740a15b416..3d0870051a 100644
--- a/library/standard/logic/axioms/hilbert.lean
+++ b/library/standard/logic/axioms/hilbert.lean
@@ -58,8 +58,8 @@ epsilon_spec (exists_intro a (refl a))
 
 theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
   ∃f, ∀x, R x (f x) :=
-let f [inline] := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
-    H [inline] := take x, epsilon_spec (H x)
+let f := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
+    H := take x, epsilon_spec (H x)
 in exists_intro f H
 
 theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
diff --git a/library/standard/struc/wf.lean b/library/standard/struc/wf.lean
index e27f1111f9..162175d735 100644
--- a/library/standard/struc/wf.lean
+++ b/library/standard/struc/wf.lean
@@ -19,7 +19,7 @@ by_contradiction (assume N : ¬∀x, P x,
   obtain (w : A) (Hw : ¬P w), from not_forall_exists N,
   -- The main "trick" is to define Q x as ¬P x.
   -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬P r)
-  let Q [inline] x := ¬P x in
+  let Q x := ¬P x in
   have Qw  : ∃w, Q w, from exists_intro w Hw,
   have Qwf : ∃min, Q min ∧ ∀b, R b min → ¬Q b, from Hwf Q Qw,
   obtain (r : A) (Hr : Q r ∧ ∀b, R b r → ¬Q b), from Qwf,
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 75c6fdfae4..4a8eed6578 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -21,7 +21,7 @@ Author: Leonardo de Moura
 namespace lean {
 namespace notation {
 static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":=");
-static name g_comma(","), g_fact("[fact]"), g_inline("[inline]"), g_from("from"), g_using("using");
+static name g_comma(","), g_fact("[fact]"), g_from("from"), g_using("using");
 static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed"), g_end("end");
 static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
 
@@ -58,14 +58,11 @@ static expr mk_let(parser & p, name const & id, expr const & t, expr const & v,
     return p.mk_app(l, v, pos);
 }
 
-static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) {
+static void parse_let_modifiers(parser & p, bool & is_fact) {
     while (true) {
         if (p.curr_is_token(g_fact)) {
             is_fact = true;
             p.next();
-        } else if (p.curr_is_token(g_inline)) {
-            is_opaque = false;
-            p.next();
         } else {
             break;
         }
@@ -79,18 +76,14 @@ static expr parse_let(parser & p, pos_info const & pos) {
     } else {
         auto pos = p.pos();
         name id  = p.check_atomic_id_next("invalid let declaration, identifier expected");
-        bool is_opaque = true;
         bool is_fact   = false;
         expr type, value;
-        parse_let_modifiers(p, is_fact, is_opaque);
+        parse_let_modifiers(p, is_fact);
         if (p.curr_is_token(g_assign)) {
             p.next();
-            if (is_opaque)
-                type  = p.save_pos(mk_expr_placeholder(), pos);
+            type  = p.save_pos(mk_expr_placeholder(), pos);
             value = p.parse_expr();
         } else if (p.curr_is_token(g_colon)) {
-            if (!is_opaque)
-                throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos());
             p.next();
             type = p.parse_expr();
             p.check_token_next(g_assign, "invalid declaration, ':=' expected");
@@ -100,28 +93,24 @@ static expr parse_let(parser & p, pos_info const & pos) {
             buffer<expr> ps;
             auto lenv = p.parse_binders(ps);
             if (p.curr_is_token(g_colon)) {
-                if (!is_opaque)
-                    throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos());
                 p.next();
                 type  = p.parse_scoped_expr(ps, lenv);
-            } else if (is_opaque) {
+            } else {
                 type  = p.save_pos(mk_expr_placeholder(), pos);
             }
             p.check_token_next(g_assign, "invalid let declaration, ':=' expected");
             value = p.parse_scoped_expr(ps, lenv);
-            if (is_opaque)
-                type  = Pi(ps, type, p);
+            type  = Pi(ps, type, p);
             value = Fun(ps, value, p);
         }
-        if (is_opaque) {
-            expr l = p.save_pos(mk_local(id, type), pos);
-            p.add_local(l);
-            expr body = abstract(parse_let_body(p, pos), l);
-            return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
-        } else  {
-            p.add_local_expr(id, value);
-            return parse_let_body(p, pos);
-        }
+        // expr l = p.save_pos(mk_local(id, type), pos);
+        // p.add_local(l);
+        // expr body = abstract(parse_let_body(p, pos), l);
+        //     return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
+        // } else  {
+        p.add_local_expr(id, value);
+        return parse_let_body(p, pos);
+        // }
     }
 }
 
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index e68f523650..bcad916338 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -1,6 +1,6 @@
 -- Correct version
-check let bool [inline]              := Type.{0},
-          and  [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,
+check let bool                      := Type.{0},
+          and  (p q : bool)         := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25             := and,
           and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
               := λ (c : bool) (H : p → q → c), H H1 H2,
@@ -10,8 +10,10 @@ check let bool [inline]              := Type.{0},
               := H q (λ (H1 : p) (H2 : q), H2)
        in and_intro
 
-check let bool [inline]                := Type.{0},
-          and  [inline] (p q : bool)   := ∀ c : bool, (p → q → c) → c,
+-- TODO(Leo): fix expected output as soon as elaborator starts checking let-expression type again
+
+check let bool                := Type.{0},
+          and  (p q : bool)   := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25               := and,
           and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p
               := λ (c : bool) (H : p → q → c), H H1 H2,
@@ -20,4 +22,3 @@ check let bool [inline]                := Type.{0},
           and_elim_right (p q : bool) (H : p ∧ q) : q
               := H q (λ (H1 : p) (H2 : q), H2)
        in and_intro
-
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 379708048d..88488e60d9 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,38 +1,8 @@
-let and_intro : ∀ (p q : Prop),
-                  p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q :=
-      λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
-        H H1 H2,
-    and_elim_left : ∀ (p q : Prop),
-                      (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
-      λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-        H p (λ (H1 : p) (H2 : q), H1),
-    and_elim_right : ∀ (p q : Prop),
-                       (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
-      λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-        H q (λ (H1 : p) (H2 : q), H2)
-in and_intro :
-  ∀ (p q : Prop),
-    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
-let1.lean:16:10: error: type mismatch at application
-  let and_intro : ∀ (p q : Prop),
-                    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
-        λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
-          H H1 H2,
-      and_elim_left : ∀ (p q : Prop),
-                        (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
-        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-          H p (λ (H1 : p) (H2 : q), H1),
-      and_elim_right : ∀ (p q : Prop),
-                         (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
-        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-          H q (λ (H1 : p) (H2 : q), H2)
-  in and_intro
-term
-  λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
-    H H1 H2
-has type
+λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+  H H1 H2 :
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)
-but is expected to have type
+λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+  H H1 H2 :
   ∀ (p q : Prop),
-    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
+    p → q → (∀ (c : Prop), (p → q → c) → c)
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 05c082f0a6..74781a12d9 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -41,7 +41,7 @@ definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
 := assume H : succ n = 0,
      have H2 : true = false, from
-     let f [inline] := (nat_rec false (fun a b, true)) in
+     let f := (nat_rec false (fun a b, true)) in
        calc true = f (succ n) : _
              ... = f 0        : {H}
              ... = false      : _,