diff -r 5d95fe89f501 -r 5e3aa998e94e LList.ML
--- a/LList.ML	Tue Dec 14 18:05:22 1993 +0100
+++ b/LList.ML	Wed Dec 22 12:43:37 1993 +0100
@@ -15,7 +15,8 @@
 (** Simplification **)
 
 val llist_simps = [case_Inl, case_Inr];
-val llist_ss = univ_ss addsimps llist_simps
+val llist_ss = univ_ss delsimps [Pair_eq] 
+                       addsimps llist_simps
                        addcongs [split_weak_cong, case_weak_cong]
                        setloop (split_tac [expand_split, expand_case]);