For each variable v in the pattern that has not been treated as a local constant, there will be an instantiation term t, such that the substitution pattern [v1 |-> t1, v2 |-> t2, ...] produces w. The effect of the tactic is to then perform abbreviations in the goal, replacing each t with the corresponding v (as long as v does not have a name beginning with an underscore character), and adding assumptions of the form Abbrev(v = t) to the goal.

Because the tactic ignores underscore variables, the user can abbreviate just those parts of the goal that are particularly relevant. Note also that the standard parser treats variables consisting of entirely underscores specially: each is expanded to a fresh name. This means that a pattern can use _ repeatedly, and it will not cause the match to look for the same instantiation for each occurrence. Nor it will require corresponding sub-terms to have the same type.