REORDER_ANTS : (term list -> term list) -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Strips universal quantifiers and antecedents of implications and reorders the antecedents
DESCRIPTION
   |- !x. a1 ==> !y. a2 ==> !z. a3 ==> !u. t
   ----------------------------------------- REORDER_ANTS rev
	   |- a3 ==> a2 ==> a1 ==> t
FAILURE
No failure. Can leave the supplied theorem unchanged.

But a choice of f other than reordering a list of terms will give a result with assumptions remaining or superfluous antecedents

COMMENTS
For simplicity, doesn’t try to reinsert quantifiers in appropriate places. If required, apply GEN_ALL to the resulting theorem.
SEEALSO
REORDER_ANTS_MOD, SPEC_ALL, GEN_ALL, UNDISCH, DISCH
HOL  Kananaskis-13