diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index ffc5cb7432..9a1e9f1860 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -9,6 +9,9 @@ import init.meta.tactic
 namespace tactic
 namespace interactive
 
+meta def intro (h : name) : tactic unit :=
+tactic.intro h >> skip
+
 meta def apply (q : pexpr) : tactic unit :=
 to_expr q >>= tactic.apply
 
@@ -18,5 +21,9 @@ tactic.refine
 meta def assumption : tactic unit :=
 tactic.assumption
 
+meta def exact (e : pexpr) : tactic unit :=
+do tgt : expr ← target,
+   to_expr_strict `((%%e : %%tgt)) >>= exact
+
 end interactive
 end tactic
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index f3d3b06a39..770d054e71 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -627,7 +627,7 @@ meta definition generalizes : list expr → tactic unit
 
 meta definition refine (e : pexpr) : tactic unit :=
 do tgt : expr ← target,
-   to_expr_core tt `((%%e : %%tgt)) >>= exact
+   to_expr `((%%e : %%tgt)) >>= exact
 
 meta definition expr_of_nat : nat → tactic expr
 | n :=
diff --git a/src/frontends/lean/begin_end_block.cpp b/src/frontends/lean/begin_end_block.cpp
index c56195df68..a74bb94867 100644
--- a/src/frontends/lean/begin_end_block.cpp
+++ b/src/frontends/lean/begin_end_block.cpp
@@ -74,8 +74,15 @@ static expr parse_tactic_interactive(parser & p, name const & decl_name) {
         if (is_explicit(binding_info(type))) {
             expr arg_type = binding_domain(type);
             if (is_constant(arg_type, get_pexpr_name())) {
+                /* auto quote expressions */
                 expr arg = parse_auto_quoted_expr(p, arity == 1 ? 0 : get_max_prec());
                 args.push_back(arg);
+            } else if (is_constant(arg_type, get_name_name())) {
+                if (!p.curr_is_identifier())
+                    throw parser_error(sstream() << "invalid tactic '" << decl_name  << "', identifier expected", p.pos());
+                name id = p.get_name_val();
+                p.next();
+                args.push_back(quote_name(id));
             } else {
                 args.push_back(p.parse_expr(get_max_prec()));
             }
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 73fa703102..3c2216b6ca 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -588,18 +588,6 @@ static expr parse_antiquote_expr(parser & p, unsigned, expr const *, pos_info co
     return p.save_pos(mk_antiquote(e), pos);
 }
 
-static expr quote_name(name const & n) {
-    if (n.is_anonymous()) {
-        return mk_constant(get_name_anonymous_name());
-    } else if (n.is_string()) {
-        expr prefix = quote_name(n.get_prefix());
-        expr str    = from_string(n.get_string());
-        return mk_app(mk_constant(get_name_mk_string_name()), str, prefix);
-    } else {
-        lean_unreachable();
-    }
-}
-
 static expr parse_quoted_name(parser & p, unsigned, expr const *, pos_info const & pos) {
     bool resolve = false;
     name id;
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 319698c930..d7c9c6dd00 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/unfold_macros.h"
 #include "library/choice.h"
+#include "library/string.h"
 #include "library/num.h"
 #include "library/util.h"
 #include "library/normalize.h"
@@ -323,4 +324,16 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg) {
 expr mk_tactic_unit() {
     return mk_app(mk_constant(get_tactic_name()), mk_constant(get_unit_name()));
 }
+
+expr quote_name(name const & n) {
+    if (n.is_anonymous()) {
+        return mk_constant(get_name_anonymous_name());
+    } else if (n.is_string()) {
+        expr prefix = quote_name(n.get_prefix());
+        expr str    = from_string(n.get_string());
+        return mk_app(mk_constant(get_name_mk_string_name()), str, prefix);
+    } else {
+        lean_unreachable();
+    }
+}
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 243ca1cd5f..e6bdc5ac94 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -102,4 +102,6 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg);
 
 /** Create (tactic unit) type */
 expr mk_tactic_unit();
+
+expr quote_name(name const & n);
 }
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index faaafd5033..f22d90ce10 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -172,6 +172,7 @@ name const * g_mul = nullptr;
 name const * g_mul_one = nullptr;
 name const * g_mul_zero = nullptr;
 name const * g_mul_zero_class = nullptr;
+name const * g_name = nullptr;
 name const * g_name_anonymous = nullptr;
 name const * g_name_mk_string = nullptr;
 name const * g_nat = nullptr;
@@ -535,6 +536,7 @@ void initialize_constants() {
     g_mul_one = new name{"mul_one"};
     g_mul_zero = new name{"mul_zero"};
     g_mul_zero_class = new name{"mul_zero_class"};
+    g_name = new name{"name"};
     g_name_anonymous = new name{"name", "anonymous"};
     g_name_mk_string = new name{"name", "mk_string"};
     g_nat = new name{"nat"};
@@ -899,6 +901,7 @@ void finalize_constants() {
     delete g_mul_one;
     delete g_mul_zero;
     delete g_mul_zero_class;
+    delete g_name;
     delete g_name_anonymous;
     delete g_name_mk_string;
     delete g_nat;
@@ -1262,6 +1265,7 @@ name const & get_mul_name() { return *g_mul; }
 name const & get_mul_one_name() { return *g_mul_one; }
 name const & get_mul_zero_name() { return *g_mul_zero; }
 name const & get_mul_zero_class_name() { return *g_mul_zero_class; }
+name const & get_name_name() { return *g_name; }
 name const & get_name_anonymous_name() { return *g_name_anonymous; }
 name const & get_name_mk_string_name() { return *g_name_mk_string; }
 name const & get_nat_name() { return *g_nat; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 4993d7ed59..7a08586b15 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -174,6 +174,7 @@ name const & get_mul_name();
 name const & get_mul_one_name();
 name const & get_mul_zero_name();
 name const & get_mul_zero_class_name();
+name const & get_name_name();
 name const & get_name_anonymous_name();
 name const & get_name_mk_string_name();
 name const & get_nat_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index cf24f8b119..7dc80c0a53 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -167,6 +167,7 @@ mul
 mul_one
 mul_zero
 mul_zero_class
+name
 name.anonymous
 name.mk_string
 nat
diff --git a/tests/lean/run/auto_quote1.lean b/tests/lean/run/auto_quote1.lean
index 32ae75aaa3..6b2ab1db87 100644
--- a/tests/lean/run/auto_quote1.lean
+++ b/tests/lean/run/auto_quote1.lean
@@ -9,8 +9,8 @@ end
 
 example (a b c : nat) : a = b → b = c → c = a :=
 begin
-  tactic.intro `h1,
-  tactic.intros,
+  intro h1,
+  intro h2,
   refine eq.symm (eq.trans h1 _),
-  assumption
+  exact h2
 end