diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean
index a963246c64..4659122c17 100644
--- a/library/init/meta/attribute.lean
+++ b/library/init/meta/attribute.lean
@@ -28,7 +28,7 @@ open tactic
 meta def register_attribute := attribute.register
 
 meta def mk_name_set_attr (attr_name : name) : command :=
-do t ← to_expr ``(caching_user_attribute name_set),
+do let t := ```(caching_user_attribute name_set),
    v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "name_set attribute",
                    mk_cache := λ ns, return (name_set.of_list ns),
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 99c19d7369..9665925f72 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -372,7 +372,7 @@ meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas
 | S (n::ns) := do S' ← S^.add_simp n, to_simp_lemmas S' ns
 
 meta def mk_simp_attr (attr_name : name) : command :=
-do t ← to_expr ``(caching_user_attribute simp_lemmas),
+do let t := ```(caching_user_attribute simp_lemmas),
    v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "simplifier attribute",
                    mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns},
diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean
index 1c4f6eaa80..6f2994a909 100644
--- a/library/init/meta/smt/ematch.lean
+++ b/library/init/meta/smt/ematch.lean
@@ -78,8 +78,8 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
   end
 
 meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
-do t ← to_expr ``(caching_user_attribute hinst_lemmas),
-   b ← if as_simp then to_expr ``(tt) else to_expr ``(ff),
+do let t := ```(caching_user_attribute hinst_lemmas),
+   let b := if as_simp then ```(tt) else ```(ff),
    v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "hinst_lemma attribute",
                    mk_cache := λ ns, to_hinst_lemmas_core reducible %%b ns hinst_lemmas.mk,
@@ -93,7 +93,7 @@ meta def mk_hinst_lemma_attrs_core (as_simp : bool) : list name → command
   (mk_hinst_lemma_attr_core n as_simp >> mk_hinst_lemma_attrs_core ns)
   <|>
   (do type ← infer_type (expr.const n []),
-      expected ← to_expr ``(caching_user_attribute hinst_lemmas),
+      let expected := ```(caching_user_attribute hinst_lemmas),
       (is_def_eq type expected
        <|> fail ("failed to create hinst_lemma attribute '" ++ n^.to_string ++ "', declaration already exists and has different type.")),
       mk_hinst_lemma_attrs_core ns)
@@ -115,9 +115,9 @@ For the ones in simp_attr_names, we use the left-hand-side of the conclusion as
 meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names : list name) (simp_attr_names : list name) : command :=
 do mk_hinst_lemma_attrs_core ff attr_names,
    mk_hinst_lemma_attrs_core tt simp_attr_names,
-   t  ← to_expr ``(caching_user_attribute hinst_lemmas),
-   l1 ← return $ quote attr_names,
-   l2 ← return $ quote simp_attr_names,
+   let t  := ```(caching_user_attribute hinst_lemmas),
+   let l1 := quote attr_names,
+   let l2 := quote simp_attr_names,
    v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "hinst_lemma attribute set",
                    mk_cache := λ ns,
diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean
index dfedee7824..e6ab9d3b4b 100644
--- a/library/init/meta/smt/rsimp.lean
+++ b/library/init/meta/smt/rsimp.lean
@@ -29,8 +29,8 @@ private meta def to_hinst_lemmas (m : transparency) (ex : name_set) : list name
     We say `ex_attr_name` is the "exception set". It is useful for excluding lemmas in `simp_attr_name`
     which are not good or redundant for ematching. -/
 meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name : name) (simp_attr_name : name) (ex_attr_name : name) : command :=
-do t  ← to_expr `(caching_user_attribute hinst_lemmas),
-   v  ← to_expr `({ name     := %%(quote attr_name),
+do let t := ```(caching_user_attribute hinst_lemmas),
+   v  ← to_expr ``({name     := %%(quote attr_name),
                     descr    := "hinst_lemma attribute derived from '" ++ to_string %%(quote simp_attr_name) ++ "'",
                     mk_cache := λ ns,
                     let aux := %%(quote simp_attr_name) in