diff -r 7af6723ad741 -r 270ec60cc9e8 src/HOLCF/Ssum.ML
--- a/src/HOLCF/Ssum.ML	Fri Jul 08 02:38:05 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Fri Jul 08 02:39:53 2005 +0200
@@ -14,7 +14,6 @@
 val cont_Iwhen3 = thm "cont_Iwhen3";
 val sinl_strict = thm "sinl_strict";
 val sinr_strict = thm "sinr_strict";
-val noteq_sinlsinr = thm "noteq_sinlsinr";
 val sinl_inject = thm "sinl_inject";
 val sinr_inject = thm "sinr_inject";
 val sinl_eq = thm "sinl_eq";