diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean
index 34259f1432..ea6ed50ea5 100644
--- a/library/init/meta/comp_value_tactics.lean
+++ b/library/init/meta/comp_value_tactics.lean
@@ -17,7 +17,7 @@ meta constant mk_int_val_ne_proof : expr → expr → option expr
 namespace tactic
 open expr
 meta def comp_val : tactic unit :=
-do t ← target,
+do t ← target >>= instantiate_mvars,
    guard (is_app t),
    type ← infer_type t.app_arg,
    (do is_def_eq type (const `nat []),