diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 05da86fd19..b4c5adfa67 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -522,7 +522,7 @@ do t ← target,
    end
 
 meta def introv : list name → tactic (list expr)
-| []      := return []
+| []      := intros_dep
 | (n::ns) := do hs ← intros_dep, h ← intro n, hs' ← introv ns, return (hs ++ h :: hs')
 
 /-- Returns n fully qualified if it refers to a constant, or else fails. -/
diff --git a/tests/lean/run/introv.lean b/tests/lean/run/introv.lean
index 3d2ac75322..ccf21f1e41 100644
--- a/tests/lean/run/introv.lean
+++ b/tests/lean/run/introv.lean
@@ -9,3 +9,10 @@ begin
   introv h₁ h₂,
   exact h₁.trans h₂
 end
+
+example : ∀ a b : nat, a = b → b = a :=
+begin
+  introv,
+  intro h,
+  exact h.symm
+end