--- a/src/ZF/Order.ML Thu May 15 15:51:09 1997 +0200 +++ b/src/ZF/Order.ML Thu May 15 15:51:47 1997 +0200 @@ -11,8 +11,6 @@ open Order; -val op addss = op unsafe_addss; - (** Basic properties of the definitions **) (*needed?*)