added Pair_eq to pair_ss in prod.ML

removed it locally in llist.ML because preconditions of the form <a,b> =
<?x,?y>, which used to be solved by reflexivity, now rewrote to a = ?x & b =
?y, which is not solved by reflexivity.

--- 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]);
 

--- a/Prod.ML	Tue Dec 14 18:05:22 1993 +0100
+++ b/Prod.ML	Wed Dec 22 12:43:37 1993 +0100
@@ -58,7 +58,7 @@
 by (rtac refl 1);
 val split = result();
 
-val pair_ss = set_ss addsimps [fst_conv, snd_conv, split];
+val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy

--- 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]);
 

--- a/prod.ML	Tue Dec 14 18:05:22 1993 +0100
+++ b/prod.ML	Wed Dec 22 12:43:37 1993 +0100
@@ -58,7 +58,7 @@
 by (rtac refl 1);
 val split = result();
 
-val pair_ss = set_ss addsimps [fst_conv, snd_conv, split];
+val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
 
 (*Prevents simplification of c: much faster*)
 val split_weak_cong = prove_goal Prod.thy