mathlib3

25a45ab7 - refactor(order/omega_complete_partial_order): remove old_structure_cmd (#9612)

refactor(order/omega_complete_partial_order): remove old_structure_cmd (#9612) Removing a use of `old_structure_cmd`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>