Removed "AddSDs [Scons_inject];" because
(a) IT WAS WRONG (should have been AddSEs)
(b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])

--- a/src/HOL/Univ.ML	Tue Apr 15 10:15:09 1997 +0200
+++ b/src/HOL/Univ.ML	Tue Apr 15 10:17:15 1997 +0200
@@ -166,8 +166,6 @@
 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
 qed "Scons_inject";
 
-AddSDs [Scons_inject];
-
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
 by (blast_tac (!claset addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";