ORDERED_REWR_CONV : (term -> term -> bool) -> thm -> term -> thm
# ADD_SYM;; val it : thm = |- !m n. m + n = n + m
# ORDERED_REWR_CONV term_order ADD_SYM `1 + 2`;; val it : thm = |- 1 + 2 = 2 + 1
# ORDERED_REWR_CONV term_order ADD_SYM `2 + 1`;; Exception: Failure "ORDERED_REWR_CONV: wrong orientation".