# HG changeset patch
# User paulson
# Date 861092235 -7200
# Node ID 58039791af82f819ac4487b5ea25ff16d91cd841
# Parent  f18035b1d531fa3ae5d80c2d9517a9adcf5f9f35
Removed "AddSDs [Scons_inject];" because
(a) IT WAS WRONG (should have been AddSEs)
(b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])

diff -r f18035b1d531 -r 58039791af82 src/HOL/Univ.ML
--- 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";