This paper extends the termination proof methods based on higher-order
reduction orderings to Nipkow's higher-order rewriting systems based
on higher-order pattern matching. Nipkow's setting is generalized so
as to allow for rules of polymorphic higher type. We successively
define: polymorphic higher-order algebras and rewrite rules; normal
higher-order reduction orderings, which are proved adequate for
proving termination of polymorphic higher-order rewriting based on
higher-order matching; a variant of the higher-order recursive path
ordering which we prove is a normal higher-order reduction ordering.