diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index 18f797641f3b7..eecf131ae7c91 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -674,6 +674,18 @@ meta def choose : expr → list name → tactic unit
   v ← get_unused_name >>= choose1 h n,
   choose v ns
 
+/--
+Instantiates metavariables that appear in the current goal.
+-/
+meta def instantiate_mvars_in_target : tactic unit :=
+target >>= instantiate_mvars >>= change
+
+/--
+Instantiates metavariables in all goals.
+-/
+meta def instantiate_mvars_in_goals : tactic unit :=
+all_goals $ instantiate_mvars_in_target
+
 /-- This makes sure that the execution of the tactic does not change the tactic state.
     This can be helpful while using rewrite, apply, or expr munging.
     Remember to instantiate your metavariables before you're done! -/
@@ -728,7 +740,7 @@ instance : monad id :=
      let out := format.to_string format!"{{ {fs} }",
      return [(out,"")] }
 
-/-- Like `resolve_name` except when the list of goals is 
+/-- Like `resolve_name` except when the list of goals is
     empty. In that situation `resolve_name` fails whereas
     `resolve_name'` simply proceeds on a dummy goal -/
 meta def resolve_name' (n : name) : tactic pexpr :=
@@ -1005,7 +1017,9 @@ private meta def tactic.use_aux (h : pexpr) : tactic unit :=
 (focus1 (refine h >> done)) <|> (fconstructor >> tactic.use_aux)
 
 protected meta def use (l : list pexpr) : tactic unit :=
-focus1 $ l.mmap' $ λ h, tactic.use_aux h <|> fail format!"failed to instantiate goal with {h}"
+focus1 $ seq (l.mmap' $ λ h, tactic.use_aux h <|> fail format!"failed to instantiate goal with {h}")
+              instantiate_mvars_in_target
+
 
 meta def clear_aux_decl_aux : list expr → tactic unit
 | []     := skip
diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean
index bb87a4c728113..26d99fb1854f1 100644
--- a/src/tactic/ring.lean
+++ b/src/tactic/ring.lean
@@ -501,7 +501,7 @@ end
   `ring!` will use a more aggressive reducibility setting to identify atoms. -/
 meta def ring (red : parse (tk "!")?) (SOP : parse ring.mode) (loc : parse location) : tactic unit :=
 match loc with
-| interactive.loc.ns [none] := ring1 red
+| interactive.loc.ns [none] := instantiate_mvars_in_target >> ring1 red
 | _ := failed
 end <|>
 do ns ← loc.get_locals,