diff -r a3899ac14a1c -r 555c8951f05c src/HOLCF/Sprod.ML
--- a/src/HOLCF/Sprod.ML	Tue Jul 12 18:20:44 2005 +0200
+++ b/src/HOLCF/Sprod.ML	Tue Jul 12 18:26:44 2005 +0200
@@ -21,7 +21,8 @@
 val ssnd_strict = thm "ssnd_strict";
 val sfst_spair = thm "sfst_spair";
 val ssnd_spair = thm "ssnd_spair";
-val sfstssnd_defined = thm "sfstssnd_defined";
+val sfst_defined = thm "sfst_defined";
+val ssnd_defined = thm "ssnd_defined";
 val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
 val less_sprod = thm "less_sprod";
 val spair_less = thm "spair_less";