`PAT_ASSUM : term -> thm_tactic -> tactic`
STRUCTURE
SYNOPSIS
Finds the first assumption that matches the term argument, applies the theorem tactic to it. The matching assumption remains in the assumption list.
DESCRIPTION
The tactic
```   PAT_ASSUM tm ttac ([A1, ..., An], g)
```
finds the first Ai which matches tm using higher-order pattern matching in the sense of ho_match_term. Free variables in the pattern that are also free in the assumptions or the goal must not be bound by the match. In effect, these variables are being treated as local constants.
FAILURE
Fails if the term doesn’t match any of the assumptions, or if the theorem-tactic fails when applied to the first assumption that does match the term.
EXAMPLE
The tactic
```   PAT_ASSUM ``x:num = y`` SUBST_ALL_TAC
```
searches the assumptions for an equality over numbers and causes its right hand side to be substituted for its left hand side throughout the goal and assumptions. It also removes the equality from the assumption list. Trying to use FIRST_ASSUM above (i.e., replacing PAT_ASSUM with FIRST_ASSUM and dropping the term argument entirely) would require that the desired equality was the first such on the list of assumptions.

If one is trying to solve the goal

```   { !x. f x = g (x + 1), !x. g x = f0 (f x)} ?- f x = g y
```
rewriting with the assumptions directly will cause a loop. Instead, one might want to rewrite with the formula for f. This can be done in an assumption-order-independent way with
```   PAT_ASSUM (Term`!x. f x = f' x`) (fn th => REWRITE_TAC [th])
```
This use of the tactic exploits higher order matching to match the RHS of the assumption, and the fact that f is effectively a local constant in the goal to find the correct assumption.