Added
AddIffs [Pair_eq];
which made
AddSEs [Pair_inject];
redundant.

--- a/src/HOL/Prod.ML	Fri Jun 06 16:02:13 1997 +0200
+++ b/src/HOL/Prod.ML	Fri Jun 06 19:30:06 1997 +0200
@@ -30,11 +30,10 @@
 by (REPEAT (ares_tac (prems@[ProdI]) 1));
 qed "Pair_inject";
 
-AddSEs [Pair_inject];
-
 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
-by (Blast_tac 1);
+by (blast_tac (!claset addSEs [Pair_inject]) 1);
 qed "Pair_eq";
+AddIffs [Pair_eq];
 
 goalw Prod.thy [fst_def] "fst((a,b)) = a";
 by (blast_tac (!claset addIs [select_equality]) 1);
@@ -88,7 +87,7 @@
 by (rtac refl 1);
 qed "split";
 
-Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
+Addsimps [fst_conv, snd_conv, split_paired_All, split];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);