diff --git a/library/init/meta/quote.lean b/library/init/meta/quote.lean
index 73ddb72439..39b3d551ff 100644
--- a/library/init/meta/quote.lean
+++ b/library/init/meta/quote.lean
@@ -48,9 +48,3 @@ meta instance : has_quote unit := ⟨λ _, ``(unit.star)⟩
 
 meta instance {α β : Type} [has_quote α] [has_quote β] : has_quote (α × β) :=
 ⟨λ ⟨x, y⟩, ``((%%(quote x), %%(quote y)))⟩
-
-meta def nat.to_expr : nat → tactic expr := λ n, to_expr $ quote n
-meta def char.to_expr : char → tactic expr := λ n, to_expr $ quote n
-meta def unsigned.to_expr : unsigned → tactic expr := λ n, to_expr $ quote n
-meta def name.to_expr : name → tactic expr := λ n, to_expr $ quote n
-meta def list_name.to_expr : list name → tactic expr := λ n, to_expr $ quote n
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 65d42658cf..f82cab4d76 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -373,8 +373,7 @@ meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas
 
 meta def mk_simp_attr (attr_name : name) : command :=
 do t ← to_expr ``(caching_user_attribute simp_lemmas),
-   a ← attr_name^.to_expr,
-   v ← to_expr ``({name     := %%a,
+   v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "simplifier attribute",
                    mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns},
                    dependencies := [`reducibility] } : caching_user_attribute simp_lemmas),
diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean
index 0d5eb2c7ff..1c4f6eaa80 100644
--- a/library/init/meta/smt/ematch.lean
+++ b/library/init/meta/smt/ematch.lean
@@ -79,9 +79,8 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
 
 meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
 do t ← to_expr ``(caching_user_attribute hinst_lemmas),
-   a ← attr_name^.to_expr,
    b ← if as_simp then to_expr ``(tt) else to_expr ``(ff),
-   v ← to_expr ``({name     := %%a,
+   v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "hinst_lemma attribute",
                    mk_cache := λ ns, to_hinst_lemmas_core reducible %%b ns hinst_lemmas.mk,
                    dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
@@ -117,10 +116,9 @@ meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names : list name) (si
 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),
-   a  ← attr_name^.to_expr,
-   l1 ← list_name.to_expr attr_names,
-   l2 ← list_name.to_expr simp_attr_names,
-   v ← to_expr ``({name     := %%a,
+   l1 ← return $ quote attr_names,
+   l2 ← return $ quote simp_attr_names,
+   v ← to_expr ``({name     := %%(quote attr_name),
                    descr    := "hinst_lemma attribute set",
                    mk_cache := λ ns,
                       let aux1 : list name := %%l1,