diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 1353a89c70..60b97556aa 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -427,10 +427,10 @@ meta def generalize2 (p : parse qexpr) (x : parse ident) (h : parse ident) : tac
 do tgt ← target,
    e ← to_expr p,
    let e' := tgt^.replace $ λa _, if a = e then some (var 1) else none,
-   to_expr `(Π x, %%p = x → %%e') >>= assert h,
+   to_expr ``(Π x, %%p = x → %%e') >>= assert h,
    swap,
    t ← get_local h,
-   exact `(%%t %%p rfl),
+   exact ``(%%t %%p rfl),
    intro x,
    intro h
 
diff --git a/library/init/meta/mk_dec_eq_instance.lean b/library/init/meta/mk_dec_eq_instance.lean
index 4ad4167ec3..377bba93d5 100644
--- a/library/init/meta/mk_dec_eq_instance.lean
+++ b/library/init/meta/mk_dec_eq_instance.lean
@@ -120,7 +120,7 @@ do env ← get_env,
            new_goal ← to_expr ``(∀ (_idx : %%I_idx_type), decidable_eq (%%I_basic_const _idx)),
            assert `_basic_dec_eq new_goal,
            swap,
-           to_expr `(_basic_dec_eq %%I_idx) >>= exact,
+           `[exact _basic_dec_eq %%I_idx],
            intro1,
            return () },
    mk_dec_eq_instance_core