diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cont.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -379,9 +379,9 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
+        (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
         (atac 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
         (atac 1),
         (rtac trans 1),
@@ -456,7 +456,7 @@
         (rtac ((hd prems) RS cont2contlub RS 
                 contlubE RS spec RS mp RS ssubst) 1),
         (atac 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (rtac ch2ch_monofun 1),
         (etac cont2mono 1),
         (atac 1),
@@ -489,7 +489,7 @@
         (rtac contlubI 1),
         (strip_tac 1),
         (rtac ext 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
         (etac spec 1),
         (atac 1),