PART_MATCH : (term -> term) -> thm -> term -> thm
PART_MATCH fn (A |- !x1...xn. t) tm
Since PART_MATCH will not instantiate variables which appear in the hypotheses of the given theorem, it fails if the attempted match would require instantiating these variables. To allow instantiation of these variables, use PART_MATCH_A.
th = |- !x. x==>x
PART_MATCH (fst o dest_imp) th "T"
|- T ==> T