src/HOLCF/Ssum2.ML

--- a/src/HOLCF/Ssum2.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Ssum2.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -16,7 +16,7 @@
         "(Isinl(x) << Isinl(y)) = (x << y)"
  (fn prems =>
         [
-        (rtac (inst_ssum_po RS ssubst) 1),
+        (stac inst_ssum_po 1),
         (rtac less_ssum2a 1)
         ]);
 
@@ -24,7 +24,7 @@
         "(Isinr(x) << Isinr(y)) = (x << y)"
  (fn prems =>
         [
-        (rtac (inst_ssum_po RS ssubst) 1),
+        (stac inst_ssum_po 1),
         (rtac less_ssum2b 1)
         ]);
 
@@ -32,7 +32,7 @@
         "(Isinl(x) << Isinr(y)) = (x = UU)"
  (fn prems =>
         [
-        (rtac (inst_ssum_po RS ssubst) 1),
+        (stac inst_ssum_po 1),
         (rtac less_ssum2c 1)
         ]);
 
@@ -40,7 +40,7 @@
         "(Isinr(x) << Isinl(y)) = (x = UU)"
  (fn prems =>
         [
-        (rtac (inst_ssum_po RS ssubst) 1),
+        (stac inst_ssum_po 1),
         (rtac less_ssum2d 1)
         ]);
 
@@ -57,7 +57,7 @@
         (rtac (less_ssum3a RS iffD2) 1),
         (rtac minimal 1),
         (hyp_subst_tac 1),
-        (rtac (strict_IsinlIsinr RS ssubst) 1),
+        (stac strict_IsinlIsinr 1),
         (rtac (less_ssum3b RS iffD2) 1),
         (rtac minimal 1)
         ]);