--- a/src/HOLCF/Sprod0.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Sprod0.ML Thu Sep 26 15:14:23 1996 +0200
@@ -225,7 +225,7 @@
"Isfst(Ispair UU y) = UU"
(fn prems =>
[
- (rtac (strict_Ispair1 RS ssubst) 1),
+ (stac strict_Ispair1 1),
(rtac strict_Isfst 1),
(rtac refl 1)
]);
@@ -234,7 +234,7 @@
"Isfst(Ispair x UU) = UU"
(fn prems =>
[
- (rtac (strict_Ispair2 RS ssubst) 1),
+ (stac strict_Ispair2 1),
(rtac strict_Isfst 1),
(rtac refl 1)
]);
@@ -259,7 +259,7 @@
"Issnd(Ispair UU y) = UU"
(fn prems =>
[
- (rtac (strict_Ispair1 RS ssubst) 1),
+ (stac strict_Ispair1 1),
(rtac strict_Issnd 1),
(rtac refl 1)
]);
@@ -268,7 +268,7 @@
"Issnd(Ispair x UU) = UU"
(fn prems =>
[
- (rtac (strict_Ispair2 RS ssubst) 1),
+ (stac strict_Ispair2 1),
(rtac strict_Issnd 1),
(rtac refl 1)
]);