--- 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),