# HG changeset patch
# User lcp
# Date 786895668 -3600
# Node ID 216ec1299bf081bba45921e57eb74c1fb726560e
# Parent  66cdfde4ec5db0065cfe1d645bcd222a67ed7225
sum_ss: deleted because it conflicts with the one in Sum.ML

diff -r 66cdfde4ec5d -r 216ec1299bf0 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Thu Dec 08 14:38:58 1994 +0100
+++ b/src/ZF/OrderArith.ML	Thu Dec 08 15:07:48 1994 +0100
@@ -62,9 +62,6 @@
 
 (** Linearity **)
 
-val sum_ss = ZF_ss addsimps [Pair_iff, InlI, InrI, Inl_iff, Inr_iff, 
-			     Inl_Inr_iff, Inr_Inl_iff];
-
 val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, 
 			       radd_Inl_Inr_iff, radd_Inr_Inl_iff];