\DOC

\TYPE {RENAME1_TAC : term quotation -> tactic}

\SYNOPSIS
Finds an instance of a pattern in a goal, and renames to use names
from the pattern.

\KEYWORDS

\DESCRIBE
The tactic {Q.RENAME1_TAC q} is defined to be
{
   MATCH_RENAME_TAC q ORELSE MATCH_ASSUM_RENAME_TAC q ORELSE
   MATCH_GOALSUB_RENAME_TAC q ORELSE MATCH_ASMSUB_RENAME_TAC q
}


\FAILURE
Fails if all of the constituent tactics fail.

\COMMENTS
This tactic can be used to force a particular set of names on a goal,
hopefully making the resulting tactic more robust in the face of
underlying implementation changes. Note though that successful use of
this tactic requires that the ``new'' names in the provided pattern
really be fresh for the goal. If one is really uncertain about what
names might be appearing in a goal, this condition may be difficult to
ensure, particularly as the tactic only looks for one instance of the pattern at a time (but see {Q.RENAME_TAC}).

This tactic is also available under the alias {bossLib.rename1}.

\SEEALSO
Q.MATCH_ASMSUB_RENAME_TAC, Q.MATCH_ASSUM_RENAME_TAC, Q.MATCH_GOALSUB_RENAME_TAC, Q.MATCH_RENAME_TAC.

\ENDDOC