diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
index 69b4ec703a..45cad89ad2 100644
--- a/library/init/meta/contradiction_tactic.lean
+++ b/library/init/meta/contradiction_tactic.lean
@@ -34,7 +34,7 @@ private meta def contra_false : list expr → tactic unit
 private meta def contra_not_a_refl_rel_a : list expr → tactic unit
 | []        := failed
 | (H :: Hs) :=
-  do t ← infer_type H >>= beta,
+  do t ← infer_type H >>= head_beta,
      (do (lhs, rhs) ← match_ne t,
          unify lhs rhs,
          tgt ← target,
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index f82cab4d76..99c19d7369 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -170,7 +170,7 @@ let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
   env   ← get_env,
   decl  ← env^.get f_name,
   new_f ← decl^.instantiate_value_univ_params f_lvls,
-  new_e ← beta (expr.mk_app new_f e^.get_app_args),
+  new_e ← head_beta (expr.mk_app new_f e^.get_app_args),
   return (u, new_e, tt)
 in do (c, new_e) ← dsimplify_core () cfg^.max_steps cfg^.visit_instances (λ c e, failed) unfold e,
       return new_e
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index f99d8e3def..f7d34dbc16 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -235,13 +235,15 @@ meta constant revert_lst    : list expr → tactic nat
 /-- Return `e` in weak head normal form with respect to the given transparency setting. -/
 meta constant whnf (e : expr) (md := semireducible) : tactic expr
 /- (head) eta expand the given expression -/
-meta constant eta_expand    : expr → tactic expr
+meta constant head_eta_expand : expr → tactic expr
 /- (head) beta reduction -/
-meta constant beta          : expr → tactic expr
+meta constant head_beta       : expr → tactic expr
 /- (head) zeta reduction -/
-meta constant zeta          : expr → tactic expr
+meta constant head_zeta       : expr → tactic expr
+/- zeta reduction -/
+meta constant zeta            : expr → tactic expr
 /- (head) eta reduction -/
-meta constant eta           : expr → tactic expr
+meta constant head_eta        : expr → tactic expr
 /-- Succeeds if `t` and `s` can be unified using the given transparency setting. -/
 meta constant unify (t s : expr) (md := semireducible) : tactic unit
 /- Similar to `unify`, but it treats metavariables as constants. -/
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index e3692cd908..c0cb93ba6b 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -320,18 +320,18 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & s0) {
     }
 }
 
-vm_obj tactic_eta_expand(vm_obj const & e, vm_obj const & s0) {
+vm_obj tactic_head_eta_expand(vm_obj const & e, vm_obj const & s0) {
     tactic_state const & s = tactic::to_state(s0);
     type_context ctx       = mk_type_context_for(s);
     try {
-        check_closed("eta_expand", to_expr(e));
+        check_closed("head_eta_expand", to_expr(e));
         return tactic::mk_success(to_obj(ctx.eta_expand(to_expr(e))), s);
     } catch (exception & ex) {
         return tactic::mk_exception(ex, s);
     }
 }
 
-vm_obj tactic_eta(vm_obj const & e, vm_obj const & s0) {
+vm_obj tactic_head_eta(vm_obj const & e, vm_obj const & s0) {
     tactic_state const & s = tactic::to_state(s0);
     try {
         return tactic::mk_success(to_obj(try_eta(to_expr(e))), s);
@@ -340,7 +340,7 @@ vm_obj tactic_eta(vm_obj const & e, vm_obj const & s0) {
     }
 }
 
-vm_obj tactic_beta(vm_obj const & e, vm_obj const & s0) {
+vm_obj tactic_head_beta(vm_obj const & e, vm_obj const & s0) {
     tactic_state const & s = tactic::to_state(s0);
     try {
         return tactic::mk_success(to_obj(annotated_head_beta_reduce(to_expr(e))), s);
@@ -349,18 +349,32 @@ vm_obj tactic_beta(vm_obj const & e, vm_obj const & s0) {
     }
 }
 
+vm_obj tactic_head_zeta(vm_obj const & e0, vm_obj const & s0) {
+    tactic_state const & s = tactic::to_state(s0);
+    try {
+        expr const & e = to_expr(e0);
+        check_closed("head_zeta", e);
+        if (!is_local(e)) return tactic::mk_success(e0, s);
+        optional<metavar_decl> mdecl = s.get_main_goal_decl();
+        if (!mdecl) return tactic::mk_success(e0, s);
+        local_context lctx = mdecl->get_context();
+        optional<local_decl> ldecl = lctx.find_local_decl(e);
+        if (!ldecl || !ldecl->get_value()) return tactic::mk_success(e0, s);
+        return tactic::mk_success(to_obj(*ldecl->get_value()), s);
+    } catch (exception & ex) {
+        return tactic::mk_exception(ex, s);
+    }
+}
+
 vm_obj tactic_zeta(vm_obj const & e0, vm_obj const & s0) {
     tactic_state const & s = tactic::to_state(s0);
     try {
         expr const & e = to_expr(e0);
         check_closed("zeta", e);
-        if (!is_local(e)) return tactic::mk_success(e0, s);
         optional<metavar_decl> mdecl = s.get_main_goal_decl();
         if (!mdecl) return tactic::mk_success(e0, s);
         local_context lctx = mdecl->get_context();
-        optional<local_decl> ldecl = lctx.find_local_decl(e);
-        if (!ldecl || !ldecl->get_value()) return tactic::mk_success(e0, s);
-        return tactic::mk_success(to_obj(*ldecl->get_value()), s);
+        return tactic::mk_success(to_obj(zeta_expand(lctx, e)), s);
     } catch (exception & ex) {
         return tactic::mk_exception(ex, s);
     }
@@ -686,9 +700,10 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}),           tactic_infer_type);
     DECLARE_VM_BUILTIN(name({"tactic", "whnf"}),                 tactic_whnf);
     DECLARE_VM_BUILTIN(name({"tactic", "is_def_eq"}),            tactic_is_def_eq);
-    DECLARE_VM_BUILTIN(name({"tactic", "eta_expand"}),           tactic_eta_expand);
-    DECLARE_VM_BUILTIN(name({"tactic", "eta"}),                  tactic_eta);
-    DECLARE_VM_BUILTIN(name({"tactic", "beta"}),                 tactic_beta);
+    DECLARE_VM_BUILTIN(name({"tactic", "head_eta_expand"}),      tactic_head_eta_expand);
+    DECLARE_VM_BUILTIN(name({"tactic", "head_eta"}),             tactic_head_eta);
+    DECLARE_VM_BUILTIN(name({"tactic", "head_beta"}),            tactic_head_beta);
+    DECLARE_VM_BUILTIN(name({"tactic", "head_zeta"}),            tactic_head_zeta);
     DECLARE_VM_BUILTIN(name({"tactic", "zeta"}),                 tactic_zeta);
     DECLARE_VM_BUILTIN(name({"tactic", "is_class"}),             tactic_is_class);
     DECLARE_VM_BUILTIN(name({"tactic", "mk_instance"}),          tactic_mk_instance);
diff --git a/tests/lean/1293.lean b/tests/lean/1293.lean
index 19c364817c..05cb66e0e9 100644
--- a/tests/lean/1293.lean
+++ b/tests/lean/1293.lean
@@ -4,7 +4,7 @@ example : true := by whnf (var 0) >> return ()
 
 example : true := by whnf (app (var 0) (var 0)) >> return ()
 
-example : true := by zeta (var 0) >> return ()
+example : true := by head_zeta (var 0) >> return ()
 
 example : true := by unify (var 0) (var 0) >> return ()
 
diff --git a/tests/lean/eta_tac.lean b/tests/lean/eta_tac.lean
index ac57f4b1b5..18dbc48d27 100644
--- a/tests/lean/eta_tac.lean
+++ b/tests/lean/eta_tac.lean
@@ -6,10 +6,10 @@ set_option pp.notation false
 
 example (a : nat) : true :=
 by do
-  mk_const `add >>= eta_expand >>= trace,
-  mk_const `nat.succ >>= eta_expand >>= trace,
-  to_expr `(add a) >>= eta_expand >>= trace,
-  to_expr `(λ x : nat, add x) >>= eta_expand >>= trace,
-  to_expr `(λ x : nat, add x) >>= eta >>= trace,
-  to_expr `(add a) >>= eta_expand >>= eta >>= trace,
+  mk_const `add >>= head_eta_expand >>= trace,
+  mk_const `nat.succ >>= head_eta_expand >>= trace,
+  to_expr `(add a) >>= head_eta_expand >>= trace,
+  to_expr `(λ x : nat, add x) >>= head_eta_expand >>= trace,
+  to_expr `(λ x : nat, add x) >>= head_eta >>= trace,
+  to_expr `(add a) >>= head_eta_expand >>= head_eta >>= trace,
   constructor
diff --git a/tests/lean/run/beta_zeta.lean b/tests/lean/run/beta_zeta.lean
index 6de2a8e7dd..9138e32741 100644
--- a/tests/lean/run/beta_zeta.lean
+++ b/tests/lean/run/beta_zeta.lean
@@ -6,15 +6,15 @@ do e ← to_expr p, guard (t = e)
 example : true :=
 let x := 10 in
 by do h ← get_local `x,
-      zeta h >>= check_expr `(10),
+      head_zeta h >>= check_expr `(10),
       triv
 
 example : let x := 10 in true :=
 by do x ← intro1,
-      zeta x >>= check_expr `(10),
+      head_zeta x >>= check_expr `(10),
       triv
 
 example : true :=
 by do h ← to_expr `((λ x : nat, x + 1) 1),
-      beta h >>= check_expr `(1 + 1),
+      head_beta h >>= check_expr `(1 + 1),
       triv