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.