term_order : term -> term -> bool
# ADD_AC;; val it : thm = |- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
# TOP_DEPTH_CONV (FIRST_CONV(map (ORDERED_REWR_CONV term_order) (CONJUNCTS ADD_AC))) `d + (f + a) + b + (c + e):num`;; val it : thm = |- d + (f + a) + b + c + e = a + b + c + d + e + f